Theorem impbid1 214

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  impbid2  215  iba  523  ibar  524  pm5.71  973  cad0  1547  19.33b  1802  19.40b  1804  19.40bOLD  1805  19.9t  2059  axc16gb  2121  19.9tOLD  2192  equs5  2339  sb4b  2346  2eu1  2541  2eu3  2543  ceqsalgALT  3204  csbprcOLD  3933  undif4  3987  ssprsseq  4297  sneqbg  4314  preq1b  4317  opthpr  4324  elpwuni  4549  disjxiun  4579  eusv2i  4789  reusv2lem3  4797  reusv3  4802  reuxfr2d  4817  soltmin  5451  ssxpb  5487  xp11  5488  xpcan  5489  xpcan2  5490  ordssun  5744  suc11  5748  unizlim  5761  iotanul  5783  imadif  5887  2elresin  5916  mpteqb  6207  f1fveq  6420  f1elima  6421  f1imass  6422  fliftf  6465  sorpssuni  6844  sorpssint  6845  iunpw  6870  ssonprc  6884  onint0  6888  oa00  7526  omcan  7536  omopth2  7551  oecan  7556  nnarcl  7583  iserd  7655  ecopoverOLD  7739  map0g  7783  fundmen  7916  fopwdom  7953  onfin  8036  fineqvlem  8059  f1finf1o  8072  isfiniteg  8105  inficl  8214  tc00  8507  cardnueq0  8673  cardsdomel  8683  wdomfil  8767  wdomnumr  8770  alephsucdom  8785  cardalephex  8796  dfac12lem2  8849  cfeq0  8961  fin23lem24  9027  fin1a2lem9  9113  carden  9252  axrepnd  9295  axacndlem4  9311  gchpwdom  9371  gchina  9400  r1tskina  9483  addcanpi  9600  mulcanpi  9601  elnpi  9689  addcan  10099  addcan2  10100  neg11  10211  negreb  10225  add20  10419  mulcand  10539  cru  10889  nn0lt10b  11316  uz11  11586  eqreznegel  11650  lbzbi  11652  rpnnen1lem6  11695  rpnnen1OLD  11701  xrmaxlt  11886  xrltmin  11887  xrmaxle  11888  xrlemin  11889  xneg11  11920  xnn0xadd0  11949  xsubge0  11963  xrub  12014  elioc2  12107  elico2  12108  elicc2  12109  fzopth  12249  2ffzeq  12329  flidz  12473  addmodlteq  12607  expeq0  12752  sq01  12848  fz1eqb  13007  hashen1  13021  hash1snb  13068  wrdnval  13190  eqwrd  13201  ccatalpha  13228  wrdl1s1  13247  ccatopth  13322  ccatopth2  13323  wrdlen2  13536  cj11  13750  sqrt0  13830  abs00  13877  recan  13924  rlimdm  14130  rpnnen2lem12  14793  0dvds  14840  dvds1  14879  alzdvds  14880  nn0enne  14932  nn0oddm1d2  14939  nnoddm1d2  14940  gcdeq0  15076  algcvgblem  15128  prmexpb  15268  prmreclem3  15460  4sqlem11  15497  moni  16219  grprcan  17278  grplcan  17300  grpinv11  17307  galcan  17560  sylow2a  17857  subgdisjb  17929  drngmuleq0  18593  lspsncmp  18937  fidomndrng  19128  coe1tm  19464  xrsdsreclb  19612  znidomb  19729  lmisfree  20000  tgdom  20593  en1top  20599  cmpfi  21021  txcmpb  21257  hmeocnvb  21387  flimcls  21599  hauspwpwf1  21601  flftg  21610  ghmcnp  21728  metrest  22139  icoopnst  22546  iocopnst  22547  ishl2  22974  vitali  23188  mbfi1fseqlem4  23291  aannenlem1  23887  perfect  24756  2lgsoddprmlem3  24939  umgrislfupgrlem  25788  usgra1v  25919  is2wlk  26095  usgra2wlkspth  26149  usg2wotspth  26411  usg2spot2nb  26592  numclwwlkun  26606  extwwlkfab  26617  grporcan  26756  grpolcan  26768  ip2eqi  27096  hial2eq  27347  eigorthi  28080  stge1i  28481  stle0i  28482  mdbr3  28540  mdbr4  28541  atsseq  28590  mdsymlem7  28652  eqvincg  28698  reuxfr3d  28713  disjunsn  28789  fpwrelmapffslem  28895  xmulcand  28960  prsdm  29288  prsrn  29289  mthmpps  30733  untangtr  30845  sltval2  31053  filnetlem4  31546  ordtopcon  31608  ordtopt0  31611  bj-dfbi6  31730  bj-19.9htbi  31881  icorempt2  32375  wl-lem-moexsb  32529  seqpo  32713  lshpcmp  33293  lsatcmp  33308  lsatcmp2  33309  ltrneq2  34452  ltrneq  34453  tendospcanN  35330  dochlkr  35692  lcfl7N  35808  hgmap11  36212  fphpd  36398  pellexlem3  36413  qirropth  36491  expdioph  36608  rpnnen3  36617  iotasbc  37642  2reu1  39835  2reu3  39837  rlimdmafv  39906  evenprm2  40161  perfectALTV  40166  nnsum3primesle9  40210  funop1  40327  fzoopth  40360  2ffzoeq  40361  usgrausgrb  40399  cplgruvtxb  40637  upgr1wlkwlkb  40848  uhgr1wlkspth  40961  usgr2wlkspth  40965  usgr2trlspth  40967  usgr2pthspth  40968  av-extwwlkfab  41520  0ringdif  41660  islinindfis  42032  lincresunit3lem3  42057  blen1b  42180