Theorem impbid1 217

Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)

Hypotheses

Ref	Expression
impbid1.1	⊢ (𝜑 → (𝜓 → 𝜒))
impbid1.2	⊢ (𝜒 → 𝜓)

Assertion

Ref	Expression
impbid1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem impbid1

Step	Hyp	Ref	Expression
1		impbid1.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		impbid1.2	. . 3 ⊢ (𝜒 → 𝜓)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜒 → 𝜓))
4	1, 3	impbid 204	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  impbid2  218  iba  520  ibar  521  pm5.71  1010  cad0  1580  19.33b  1848  19.40b  1851  19.9t  2133  axc16gb  2189  equs5  2397  2eu1  2682  2eu1OLD  2683  2eu3  2685  2eu3OLD  2686  ceqsalgALT  3445  eqvincg  3550  reuxfr3d  3645  2reu1  3778  disjeq0  4282  undif4  4293  ssprsseq  4626  sneqbg  4642  preq1b  4645  opthpr  4650  preq12nebg  4661  opthprneg  4663  elpwuni  4887  disjxiun  4920  eusv2i  5142  reusv2lem3  5148  reusv3  5153  soltmin  5830  ssxpb  5865  xp11  5866  xpcan  5867  xpcan2  5868  ordssun  6122  suc11  6126  unizlim  6139  imadif  6265  2elresin  6295  mpteqb  6607  f1fveq  6839  f1elima  6840  f1imass  6841  fliftf  6885  sorpssuni  7270  sorpssint  7271  iunpw  7303  ssonprc  7317  onint0  7321  oa00  7980  omcan  7990  omopth2  8005  oecan  8010  nnarcl  8037  iserd  8109  map0g  8241  fundmen  8374  fopwdom  8415  onfin  8498  fineqvlem  8521  f1finf1o  8534  isfiniteg  8567  inficl  8678  tc00  8978  cardnueq0  9181  cardsdomel  9191  wdomfil  9275  wdomnumr  9278  alephsucdom  9293  cardalephex  9304  dfac12lem2  9358  cfeq0  9470  fin23lem24  9536  fin1a2lem9  9622  carden  9765  axrepnd  9808  axacndlem4  9824  gchpwdom  9884  gchina  9913  r1tskina  9996  addcanpi  10113  mulcanpi  10114  elnpi  10202  addcan  10618  addcan2  10619  neg11  10732  negreb  10746  add20  10947  mulcand  11068  cru  11425  nn0lt10b  11851  uz11  12075  eqreznegel  12142  lbzbi  12144  rpnnen1lem6  12190  xrmaxlt  12385  xrltmin  12386  xrmaxle  12387  xrlemin  12388  xneg11  12419  xnn0xadd0  12450  xsubge0  12464  xrub  12515  elioc2  12609  elico2  12610  elicc2  12611  fzopth  12754  2ffzeq  12838  flidz  12989  addmodlteq  13123  expeq0  13268  sq01  13395  fz1eqb  13524  hashen1  13539  hash1snb  13587  hashle2pr  13640  wrdnval  13701  eqwrd  13714  ccatalpha  13750  wrdl1s1  13771  ccats1alpha  13776  ccatopth  13901  ccatopthOLD  13902  ccatopth2  13903  wrdlen2  14162  cj11  14376  sqrt0  14456  abs00  14504  recan  14551  cnsqrt00  14607  rlimdm  14763  rpnnen2lem12  15432  0dvds  15484  dvds1  15523  alzdvds  15524  nn0enne  15582  nn0oddm1d2  15590  nnoddm1d2  15591  gcdeq0  15719  algcvgblem  15771  2mulprm  15887  prmexpb  15912  prmreclem3  16104  4sqlem11  16141  moni  16858  grprcan  17918  grplcan  17942  grpinv11  17949  galcan  18199  sylow2a  18499  subgdisjb  18571  drngmuleq0  19242  lspsncmp  19604  fidomndrng  19795  coe1tm  20138  xrsdsreclb  20288  znidomb  20404  lmisfree  20682  tgdom  21284  en1top  21290  cmpfi  21714  txcmpb  21950  hmeocnvb  22080  flimcls  22291  hauspwpwf1  22293  flftg  22302  ghmcnp  22420  metrest  22831  icoopnst  23240  iocopnst  23241  ishl2  23670  vitali  23911  mbfi1fseqlem4  24016  aannenlem1  24614  perfect  25503  2lgsoddprmlem3  25686  2sq2  25705  umgrislfupgrlem  26604  usgrausgrb  26651  upgriswlk  27119  uhgrwkspth  27238  usgr2wlkspth  27242  usgr2trlspth  27244  usgr2pthspth  27245  extwwlkfab  27885  extwwlkfabOLD  27886  grporcan  28066  grpolcan  28078  ip2eqi  28405  hial2eq  28656  eigorthi  29389  stge1i  29790  stle0i  29791  mdbr3  29849  mdbr4  29850  atsseq  29899  mdsymlem7  29961  disjunsn  30104  fpwrelmapffslem  30221  xmulcand  30344  prsdm  30801  prsrn  30802  mthmpps  32349  untangtr  32460  funeldmb  32526  sltval2  32684  filnetlem4  33250  ordtopconn  33307  ordtopt0  33310  bj-dfbi6  33425  bj-19.9htbi  33547  icorempo  34074  inunissunidif  34098  fvineqsneu  34133  wl-lem-moexsb  34245  seqpo  34464  lshpcmp  35569  lsatcmp  35584  lsatcmp2  35585  ltrneq2  36729  ltrneq  36730  tendospcanN  37604  dochlkr  37966  lcfl7N  38082  hgmap11  38483  ccatcan2d  38572  remulcan2d  38593  resubcan2  38649  fphpd  38809  pellexlem3  38824  qirropth  38901  expdioph  39016  rpnnen3  39025  iotasbc  40168  2reu3  42715  rlimdmafv  42782  afv2orxorb  42833  rlimdmafv2  42863  funop1  42888  fzoopth  42933  2ffzoeq  42934  prprelprb  43047  poprelb  43054  evenprm2  43247  perfectALTV  43256  nnsum3primesle9  43327  upgrwlkupwlkb  43384  0ringdif  43505  islinindfis  43871  lincresunit3lem3  43896  blen1b  44016  line2ylem  44106  line2y  44110