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  529  pm5.61  1000  pm5.71  1027  cad0  1620  cad0OLD  1621  19.33b  1889  19.40b  1892  19.9t  2198  axc16gb  2254  equs5  2460  2eu1  2647  2eu1v  2648  2eu3  2650  ceqsalgALT  3509  eqvincg  3636  reuxfrd  3744  2reu1  3891  disjeq0  4455  undif4  4466  ssprsseq  4828  sneqbg  4844  preq1b  4847  opthpr  4852  preq12nebg  4863  opthprneg  4865  dfiun2g  5033  elpwuni  5108  disjxiun  5145  eusv2i  5392  reusv2lem3  5398  reusv3  5403  soltmin  6135  ssxpb  6171  xp11  6172  xpcan  6173  xpcan2  6174  ordssun  6464  suc11  6469  unizlim  6485  imadif  6630  2elresin  6669  mpteqb  7015  f1fveq  7258  f1elima  7259  f1imass  7260  fliftf  7309  funeldmb  7353  sorpssuni  7719  sorpssint  7720  iunpw  7755  ssonprc  7772  onint0  7776  oa00  8556  omcan  8566  omopth2  8581  oecan  8586  nnarcl  8613  iserd  8726  mapfset  8841  map0g  8875  fundmen  9028  fopwdom  9077  onfin  9227  0sdom1dom  9235  fineqvlem  9259  f1finf1o  9268  f1finf1oOLD  9269  isfiniteg  9301  inficl  9417  tc00  9740  cardnueq0  9956  cardsdomel  9966  wdomfil  10053  wdomnumr  10056  alephsucdom  10071  cardalephex  10082  dfac12lem2  10136  cfeq0  10248  fin23lem24  10314  fin1a2lem9  10400  carden  10543  axrepnd  10586  axacndlem4  10602  gchpwdom  10662  gchina  10691  r1tskina  10774  addcanpi  10891  mulcanpi  10892  elnpi  10980  addcan  11395  addcan2  11396  neg11  11508  negreb  11522  add20  11723  mulcand  11844  cru  12201  nn0lt10b  12621  uz11  12844  eqreznegel  12915  lbzbi  12917  rpnnen1lem6  12963  xrmaxlt  13157  xrltmin  13158  xrmaxle  13159  xrlemin  13160  xneg11  13191  xnn0xadd0  13223  xsubge0  13237  xrub  13288  elioc2  13384  elico2  13385  elicc2  13386  fzopth  13535  2ffzeq  13619  flidz  13772  addmodlteq  13908  expeq0  14055  sq01  14185  fz1eqb  14311  hashen1  14327  hash1snb  14376  hashle2pr  14435  wrdnval  14492  eqwrd  14504  ccatalpha  14540  wrdl1s1  14561  ccats1alpha  14566  ccatopth  14663  ccatopth2  14664  wrdlen2  14892  cj11  15106  sqrt0  15185  abs00  15233  recan  15280  cnsqrt00  15336  rlimdm  15492  rpnnen2lem12  16165  0dvds  16217  dvds1  16259  alzdvds  16260  nn0enne  16317  nn0oddm1d2  16325  nnoddm1d2  16326  gcdeq0  16455  algcvgblem  16511  2mulprm  16627  prmexpb  16654  prmreclem3  16848  4sqlem11  16885  moni  17680  grprcan  18855  grplcan  18882  grpinv11  18889  galcan  19163  sylow2a  19482  subgdisjb  19556  drngmuleq0  20339  lspsncmp  20722  fidomndrng  20919  xrsdsreclb  20985  znidomb  21109  lmisfree  21389  coe1tm  21787  tgdom  22473  en1top  22479  cmpfi  22904  txcmpb  23140  hmeocnvb  23270  flimcls  23481  hauspwpwf1  23483  flftg  23492  ghmcnp  23611  metrest  24025  icoopnst  24447  iocopnst  24448  ishl2  24879  vitali  25122  mbfi1fseqlem4  25228  aannenlem1  25833  perfect  26724  2lgsoddprmlem3  26907  2sq2  26926  sltval2  27149  bday0b  27321  negs11  27513  umgrislfupgrlem  28372  usgrausgrb  28419  upgriswlk  28888  uhgrwkspth  29002  usgr2wlkspth  29006  usgr2trlspth  29008  usgr2pthspth  29009  extwwlkfab  29595  grporcan  29759  grpolcan  29771  ip2eqi  30097  hial2eq  30347  eigorthi  31078  stge1i  31479  stle0i  31480  mdbr3  31538  mdbr4  31539  atsseq  31588  mdsymlem7  31650  reuxfrdf  31719  disjunsn  31813  fpwrelmapffslem  31945  xmulcand  32075  prsdm  32883  prsrn  32884  lfuhgr  34097  lfuhgr2  34098  mthmpps  34562  untangtr  34672  filnetlem4  35255  ordtopconn  35313  ordtopt0  35316  bj-dfbi6  35441  bj-19.9htbi  35570  bj-elid6  36040  icorempo  36221  inunissunidif  36245  fvineqsneu  36281  wl-lem-moexsb  36422  seqpo  36604  lshpcmp  37847  lsatcmp  37862  lsatcmp2  37863  ltrneq2  39008  ltrneq  39009  tendospcanN  39883  dochlkr  40245  lcfl7N  40361  hgmap11  40762  ccatcan2d  41067  remulcan2d  41175  resubcan2  41258  readdcan2  41282  sn-addcand  41289  sn-addcan2d  41291  remulcand  41308  itrere  41336  retire  41337  cnreeu  41338  fphpd  41540  pellexlem3  41555  qirropth  41632  expdioph  41748  rpnnen3  41757  iotasbc  43164  f1ocof1ob2  45777  2reu3  45805  rlimdmafv  45872  afv2orxorb  45923  rlimdmafv2  45953  funop1  45978  fzoopth  46022  2ffzoeq  46023  prprelprb  46172  poprelb  46179  evenprm2  46369  perfectALTV  46378  nnsum3primesle9  46449  upgrwlkupwlkb  46506  0ringdif  46631  islinindfis  47084  lincresunit3lem3  47109  blen1b  47228  line2ylem  47391  line2y  47395  intubeu  47563  unilbeu  47564  thincn0eu  47606