Theorem ibar 504

Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)

Assertion

Ref	Expression
ibar

Proof of Theorem ibar

Step	Hyp	Ref	Expression
1		pm3.2 447	. 2
2		simpr 461	. 2
3	1, 2	impbid1 203	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  biantrur  506  biantrurd  508  anclb  547  pm5.42  548  anabs5  809  pm5.33  878  bianabs  880  baib  903  baibd  909  pclem6  930  cad1  1465  moanim  2350  euan  2351  eueq3  3274  ifan  3987  dfopif  4214  reusv2lem5  4657  fvopab3g  5952  riota1a  6277  dfom2  6702  suppssr  6950  mpt2curryd  7017  boxcutc  7532  funisfsupp  7854  dfac3  8523  eluz2  11116  elixx3g  11571  elfz2  11708  zmodid2  12024  shftfib  12905  sadadd2lem2  14100  smumullem  14142  issubg  16201  resgrpisgrp  16222  sscntz  16364  pgrpsubgsymgbi  16432  issubrg  17429  lindsmm  18863  mdetunilem8  19121  mdetunilem9  19122  cmpsub  19900  txcnmpt  20125  fbfinnfr  20342  elfilss  20377  fixufil  20423  ibladdlem  22226  iblabslem  22234  sgmss  23380  cusgra2v  24462  eclclwwlkn1  24832  el2wlkonotot  24873  rusgranumwlklem0  24948  eupath2lem1  24977  frgra3v  25002  pjimai  27095  chrelati  27283  tltnle  27650  metidv  27871  cnambfre  30063  itg2addnclem2  30067  ibladdnclem  30071  iblabsnclem  30078  divalgmodcl  30929  expdiophlem1  30963  reuan  32185  isrnghm  32698  rnghmval2  32701  uzlidlring  32735  islindeps  33054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371