Theorem impbid1 225

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  impbid2  226  iba  527  pm5.61  1002  pm5.71  1029  cad0  1619  19.33b  1886  19.40b  1889  19.9t  2209  axc16gb  2267  equs5  2462  2eu1  2649  2eu1v  2650  2eu3  2652  ceqsalgALT  3475  eqvincg  3600  reuxfrd  3704  2reu1  3845  disjeq0  4406  undif4  4417  iftrueb  4490  ssprsseq  4779  sneqbg  4797  preq1b  4800  opthpr  4805  preq12nebg  4817  opthprneg  4819  dfiun2g  4983  elpwuni  5058  disjxiun  5093  eusv2i  5337  reusv2lem3  5343  reusv3  5348  soltmin  6091  ssxpb  6130  xp11  6131  xpcan  6132  xpcan2  6133  ordssun  6419  suc11  6424  unizlim  6439  imadif  6574  2elresin  6611  mpteqb  6958  f1fveq  7206  f1elima  7207  f1imass  7208  fliftf  7259  funeldmb  7303  sorpssuni  7675  sorpssint  7676  iunpw  7714  ssonprc  7730  onint0  7734  oa00  8484  omcan  8494  omopth2  8509  oecan  8515  nnarcl  8542  iserd  8659  mapfset  8785  map0g  8820  fundmen  8966  fopwdom  9011  onfin  9137  0sdom1dom  9144  fineqvlem  9164  f1finf1o  9171  isfiniteg  9198  inficl  9326  tc00  9653  cardnueq0  9874  cardsdomel  9884  wdomfil  9969  wdomnumr  9972  alephsucdom  9987  cardalephex  9998  dfac12lem2  10053  cfeq0  10164  fin23lem24  10230  fin1a2lem9  10316  carden  10459  axrepnd  10503  axacndlem4  10519  gchpwdom  10579  gchina  10608  r1tskina  10691  addcanpi  10808  mulcanpi  10809  elnpi  10897  addcan  11315  addcan2  11316  neg11  11430  negreb  11444  add20  11647  mulcand  11768  cru  12135  nn0lt10b  12552  uz11  12774  eqreznegel  12845  lbzbi  12847  rpnnen1lem6  12893  xrmaxlt  13094  xrltmin  13095  xrmaxle  13096  xrlemin  13097  xneg11  13128  xnn0xadd0  13160  xsubge0  13174  xrub  13225  elioc2  13323  elico2  13324  elicc2  13325  fzopth  13475  2ffzeq  13563  fzoopth  13676  flidz  13728  addmodlteq  13867  expeq0  14013  sq01  14146  fz1eqb  14275  hashen1  14291  hash1snb  14340  hashle2pr  14398  wrdnval  14466  eqwrd  14478  ccatalpha  14515  wrdl1s1  14536  ccats1alpha  14541  ccatopth  14637  ccatopth2  14638  wrdlen2  14865  cj11  15083  sqrt0  15162  abs00  15210  recan  15258  cnsqrt00  15314  rlimdm  15472  rpnnen2lem12  16148  0dvds  16201  dvds1  16244  alzdvds  16245  nn0enne  16302  nn0oddm1d2  16310  nnoddm1d2  16311  gcdeq0  16442  algcvgblem  16502  2mulprm  16618  prmexpb  16644  prmreclem3  16844  4sqlem11  16881  moni  17658  chnfibg  18557  grprcan  18901  grplcan  18928  grpinv11  18935  grpinv11OLD  18936  galcan  19231  sylow2a  19546  subgdisjb  19620  0ringdif  20458  domnlcanb  20651  domnrcanb  20653  drngmuleq0  20694  fidomndrng  20704  lspsncmp  21069  xrsdsreclb  21366  znidomb  21514  lmisfree  21795  coe1tm  22213  tgdom  22920  en1top  22926  cmpfi  23350  txcmpb  23586  hmeocnvb  23716  flimcls  23927  hauspwpwf1  23929  flftg  23938  ghmcnp  24057  metrest  24466  icoopnst  24890  iocopnst  24891  ishl2  25324  vitali  25568  mbfi1fseqlem4  25673  aannenlem1  26290  perfect  27196  2lgsoddprmlem3  27379  2sq2  27398  sltval2  27622  bday0b  27801  negs11  28018  elnns2  28301  n0cutlt  28318  umgrislfupgrlem  29144  usgrausgrb  29191  upgriswlk  29663  uhgrwkspth  29777  usgr2wlkspth  29781  usgr2trlspth  29783  usgr2pthspth  29784  extwwlkfab  30376  grporcan  30542  grpolcan  30554  ip2eqi  30880  hial2eq  31130  eigorthi  31861  stge1i  32262  stle0i  32263  mdbr3  32321  mdbr4  32322  atsseq  32371  mdsymlem7  32433  reuxfrdf  32514  disjunsn  32618  fpwrelmapffslem  32760  xmulcand  32951  prsdm  34020  prsrn  34021  lfuhgr  35261  lfuhgr2  35262  mthmpps  35725  untangtr  35857  filnetlem4  36524  ordtopconn  36582  ordtopt0  36585  bj-dfbi6  36718  bj-19.9htbi  36847  bj-elid6  37314  icorempo  37495  inunissunidif  37519  fvineqsneu  37555  wl-lem-moexsb  37712  seqpo  37887  lshpcmp  39187  lsatcmp  39202  lsatcmp2  39203  ltrneq2  40347  ltrneq  40348  tendospcanN  41222  dochlkr  41584  lcfl7N  41700  hgmap11  42101  ccatcan2d  42448  remulcan2d  42454  itrere  42515  log11d  42543  resubcan2  42585  readdcan2  42610  sn-addcand  42617  sn-addcan2d  42619  remulcand  42636  sn-itrere  42685  sn-retire  42686  cnreeu  42687  fphpd  43000  pellexlem3  43015  qirropth  43092  expdioph  43207  rpnnen3  43216  iotasbc  44602  f1ocof1ob2  47270  2reu3  47298  rlimdmafv  47365  afv2orxorb  47416  rlimdmafv2  47446  funop1  47471  2ffzoeq  47515  prprelprb  47705  poprelb  47712  evenprm2  47902  perfectALTV  47911  nnsum3primesle9  47982  upgrwlkupwlkb  48329  islinindfis  48637  lincresunit3lem3  48662  blen1b  48776  line2ylem  48939  line2y  48943  intubeu  49171  unilbeu  49172  thincn0eu  49618