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  527  pm5.61  998  pm5.71  1025  cad0  1618  cad0OLD  1619  19.33b  1887  19.40b  1890  19.9t  2196  axc16gb  2252  equs5  2458  2eu1  2645  2eu1v  2646  2eu3  2648  ceqsalgALT  3508  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  6137  ssxpb  6173  xp11  6174  xpcan  6175  xpcan2  6176  ordssun  6466  suc11  6471  unizlim  6487  imadif  6632  2elresin  6671  mpteqb  7017  f1fveq  7264  f1elima  7265  f1imass  7266  fliftf  7315  funeldmb  7359  sorpssuni  7726  sorpssint  7727  iunpw  7762  ssonprc  7779  onint0  7783  oa00  8565  omcan  8575  omopth2  8590  oecan  8595  nnarcl  8622  iserd  8735  mapfset  8850  map0g  8884  fundmen  9037  fopwdom  9086  onfin  9236  0sdom1dom  9244  fineqvlem  9268  f1finf1o  9277  f1finf1oOLD  9278  isfiniteg  9310  inficl  9426  tc00  9749  cardnueq0  9965  cardsdomel  9975  wdomfil  10062  wdomnumr  10065  alephsucdom  10080  cardalephex  10091  dfac12lem2  10145  cfeq0  10257  fin23lem24  10323  fin1a2lem9  10409  carden  10552  axrepnd  10595  axacndlem4  10611  gchpwdom  10671  gchina  10700  r1tskina  10783  addcanpi  10900  mulcanpi  10901  elnpi  10989  addcan  11405  addcan2  11406  neg11  11518  negreb  11532  add20  11733  mulcand  11854  cru  12211  nn0lt10b  12631  uz11  12854  eqreznegel  12925  lbzbi  12927  rpnnen1lem6  12973  xrmaxlt  13167  xrltmin  13168  xrmaxle  13169  xrlemin  13170  xneg11  13201  xnn0xadd0  13233  xsubge0  13247  xrub  13298  elioc2  13394  elico2  13395  elicc2  13396  fzopth  13545  2ffzeq  13629  flidz  13782  addmodlteq  13918  expeq0  14065  sq01  14195  fz1eqb  14321  hashen1  14337  hash1snb  14386  hashle2pr  14445  wrdnval  14502  eqwrd  14514  ccatalpha  14550  wrdl1s1  14571  ccats1alpha  14576  ccatopth  14673  ccatopth2  14674  wrdlen2  14902  cj11  15116  sqrt0  15195  abs00  15243  recan  15290  cnsqrt00  15346  rlimdm  15502  rpnnen2lem12  16175  0dvds  16227  dvds1  16269  alzdvds  16270  nn0enne  16327  nn0oddm1d2  16335  nnoddm1d2  16336  gcdeq0  16465  algcvgblem  16521  2mulprm  16637  prmexpb  16664  prmreclem3  16858  4sqlem11  16895  moni  17690  grprcan  18901  grplcan  18928  grpinv11  18935  galcan  19216  sylow2a  19535  subgdisjb  19609  0ringdif  20423  drngmuleq0  20614  lspsncmp  20963  fidomndrng  21216  xrsdsreclb  21282  znidomb  21428  lmisfree  21708  coe1tm  22116  tgdom  22802  en1top  22808  cmpfi  23233  txcmpb  23469  hmeocnvb  23599  flimcls  23810  hauspwpwf1  23812  flftg  23821  ghmcnp  23940  metrest  24354  icoopnst  24784  iocopnst  24785  ishl2  25219  vitali  25463  mbfi1fseqlem4  25569  aannenlem1  26181  perfect  27079  2lgsoddprmlem3  27262  2sq2  27281  sltval2  27504  bday0b  27678  negs11  27876  elnns2  28095  umgrislfupgrlem  28817  usgrausgrb  28864  upgriswlk  29333  uhgrwkspth  29447  usgr2wlkspth  29451  usgr2trlspth  29453  usgr2pthspth  29454  extwwlkfab  30040  grporcan  30206  grpolcan  30218  ip2eqi  30544  hial2eq  30794  eigorthi  31525  stge1i  31926  stle0i  31927  mdbr3  31985  mdbr4  31986  atsseq  32035  mdsymlem7  32097  reuxfrdf  32166  disjunsn  32260  fpwrelmapffslem  32392  xmulcand  32522  prsdm  33360  prsrn  33361  lfuhgr  34574  lfuhgr2  34575  mthmpps  35039  untangtr  35155  filnetlem4  35733  ordtopconn  35791  ordtopt0  35794  bj-dfbi6  35919  bj-19.9htbi  36048  bj-elid6  36518  icorempo  36699  inunissunidif  36723  fvineqsneu  36759  wl-lem-moexsb  36900  seqpo  37082  lshpcmp  38325  lsatcmp  38340  lsatcmp2  38341  ltrneq2  39486  ltrneq  39487  tendospcanN  40361  dochlkr  40723  lcfl7N  40839  hgmap11  41240  ccatcan2d  41539  remulcan2d  41643  resubcan2  41727  readdcan2  41751  sn-addcand  41758  sn-addcan2d  41760  remulcand  41777  itrere  41805  retire  41806  cnreeu  41807  fphpd  42020  pellexlem3  42035  qirropth  42112  expdioph  42228  rpnnen3  42237  iotasbc  43644  f1ocof1ob2  46252  2reu3  46280  rlimdmafv  46347  afv2orxorb  46398  rlimdmafv2  46428  funop1  46453  fzoopth  46497  2ffzoeq  46498  prprelprb  46647  poprelb  46654  evenprm2  46844  perfectALTV  46853  nnsum3primesle9  46924  upgrwlkupwlkb  46981  islinindfis  47295  lincresunit3lem3  47320  blen1b  47439  line2ylem  47602  line2y  47606  intubeu  47774  unilbeu  47775  thincn0eu  47817