Theorem impbid1 224

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 211	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  impbid2  225  iba  528  pm5.61  998  pm5.71  1025  cad0  1620  cad0OLD  1621  19.33b  1889  19.40b  1892  19.9t  2198  axc16gb  2255  equs5  2461  2eu1  2653  2eu1v  2654  2eu3  2656  ceqsalgALT  3466  eqvincg  3579  reuxfrd  3684  2reu1  3831  disjeq0  4390  undif4  4401  ssprsseq  4759  sneqbg  4775  preq1b  4778  opthpr  4783  preq12nebg  4794  opthprneg  4796  dfiun2g  4961  elpwuni  5035  disjxiun  5072  eusv2i  5318  reusv2lem3  5324  reusv3  5329  soltmin  6046  ssxpb  6082  xp11  6083  xpcan  6084  xpcan2  6085  ordssun  6369  suc11  6373  unizlim  6387  imadif  6525  2elresin  6562  mpteqb  6903  f1fveq  7144  f1elima  7145  f1imass  7146  fliftf  7195  sorpssuni  7594  sorpssint  7595  iunpw  7630  ssonprc  7646  onint0  7650  oa00  8399  omcan  8409  omopth2  8424  oecan  8429  nnarcl  8456  iserd  8533  mapfset  8647  map0g  8681  fundmen  8830  fopwdom  8876  onfin  9022  fineqvlem  9046  f1finf1o  9055  isfiniteg  9083  inficl  9193  tc00  9515  cardnueq0  9731  cardsdomel  9741  wdomfil  9826  wdomnumr  9829  alephsucdom  9844  cardalephex  9855  dfac12lem2  9909  cfeq0  10021  fin23lem24  10087  fin1a2lem9  10173  carden  10316  axrepnd  10359  axacndlem4  10375  gchpwdom  10435  gchina  10464  r1tskina  10547  addcanpi  10664  mulcanpi  10665  elnpi  10753  addcan  11168  addcan2  11169  neg11  11281  negreb  11295  add20  11496  mulcand  11617  cru  11974  nn0lt10b  12391  uz11  12616  eqreznegel  12683  lbzbi  12685  rpnnen1lem6  12731  xrmaxlt  12924  xrltmin  12925  xrmaxle  12926  xrlemin  12927  xneg11  12958  xnn0xadd0  12990  xsubge0  13004  xrub  13055  elioc2  13151  elico2  13152  elicc2  13153  fzopth  13302  2ffzeq  13386  flidz  13539  addmodlteq  13675  expeq0  13822  sq01  13949  fz1eqb  14078  hashen1  14094  hash1snb  14143  hashle2pr  14200  wrdnval  14257  eqwrd  14269  ccatalpha  14307  wrdl1s1  14328  ccats1alpha  14333  ccatopth  14438  ccatopth2  14439  wrdlen2  14666  cj11  14882  sqrt0  14962  abs00  15010  recan  15057  cnsqrt00  15113  rlimdm  15269  rpnnen2lem12  15943  0dvds  15995  dvds1  16037  alzdvds  16038  nn0enne  16095  nn0oddm1d2  16103  nnoddm1d2  16104  gcdeq0  16233  algcvgblem  16291  2mulprm  16407  prmexpb  16434  prmreclem3  16628  4sqlem11  16665  moni  17457  grprcan  18622  grplcan  18646  grpinv11  18653  galcan  18919  sylow2a  19233  subgdisjb  19308  drngmuleq0  20023  lspsncmp  20387  fidomndrng  20588  xrsdsreclb  20654  znidomb  20778  lmisfree  21058  coe1tm  21453  tgdom  22137  en1top  22143  cmpfi  22568  txcmpb  22804  hmeocnvb  22934  flimcls  23145  hauspwpwf1  23147  flftg  23156  ghmcnp  23275  metrest  23689  icoopnst  24111  iocopnst  24112  ishl2  24543  vitali  24786  mbfi1fseqlem4  24892  aannenlem1  25497  perfect  26388  2lgsoddprmlem3  26571  2sq2  26590  umgrislfupgrlem  27501  usgrausgrb  27548  upgriswlk  28017  uhgrwkspth  28132  usgr2wlkspth  28136  usgr2trlspth  28138  usgr2pthspth  28139  extwwlkfab  28725  grporcan  28889  grpolcan  28901  ip2eqi  29227  hial2eq  29477  eigorthi  30208  stge1i  30609  stle0i  30610  mdbr3  30668  mdbr4  30669  atsseq  30718  mdsymlem7  30780  reuxfrdf  30848  disjunsn  30942  fpwrelmapffslem  31076  xmulcand  31204  prsdm  31873  prsrn  31874  lfuhgr  33088  lfuhgr2  33089  mthmpps  33553  untangtr  33664  funeldmb  33746  sltval2  33868  bday0b  34033  filnetlem4  34579  ordtopconn  34637  ordtopt0  34640  bj-dfbi6  34765  bj-19.9htbi  34894  bj-elid6  35350  icorempo  35531  inunissunidif  35555  fvineqsneu  35591  wl-lem-moexsb  35732  seqpo  35914  lshpcmp  37009  lsatcmp  37024  lsatcmp2  37025  ltrneq2  38169  ltrneq  38170  tendospcanN  39044  dochlkr  39406  lcfl7N  39522  hgmap11  39923  ccatcan2d  40226  remulcan2d  40300  resubcan2  40378  readdcan2  40402  sn-addcand  40408  sn-addcan2d  40410  remulcand  40427  itrere  40443  retire  40444  cnreeu  40445  fphpd  40645  pellexlem3  40660  qirropth  40737  expdioph  40852  rpnnen3  40861  iotasbc  42044  f1ocof1ob2  44585  2reu3  44613  rlimdmafv  44680  afv2orxorb  44731  rlimdmafv2  44761  funop1  44786  fzoopth  44830  2ffzoeq  44831  prprelprb  44980  poprelb  44987  evenprm2  45177  perfectALTV  45186  nnsum3primesle9  45257  upgrwlkupwlkb  45314  0ringdif  45439  islinindfis  45801  lincresunit3lem3  45826  blen1b  45945  line2ylem  46108  line2y  46112  intubeu  46281  unilbeu  46282  thincn0eu  46324