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  2211  axc16gb  2269  equs5  2464  2eu1  2651  2eu1v  2652  2eu3  2654  ceqsalgALT  3477  eqvincg  3602  reuxfrd  3706  2reu1  3847  disjeq0  4408  undif4  4419  iftrueb  4492  ssprsseq  4781  sneqbg  4799  preq1b  4802  opthpr  4807  preq12nebg  4819  opthprneg  4821  dfiun2g  4985  elpwuni  5060  disjxiun  5095  eusv2i  5339  reusv2lem3  5345  reusv3  5350  soltmin  6093  ssxpb  6132  xp11  6133  xpcan  6134  xpcan2  6135  ordssun  6421  suc11  6426  unizlim  6441  imadif  6576  2elresin  6613  mpteqb  6960  f1fveq  7208  f1elima  7209  f1imass  7210  fliftf  7261  funeldmb  7305  sorpssuni  7677  sorpssint  7678  iunpw  7716  ssonprc  7732  onint0  7736  oa00  8486  omcan  8496  omopth2  8511  oecan  8517  nnarcl  8544  iserd  8662  mapfset  8789  map0g  8824  fundmen  8970  fopwdom  9015  onfin  9141  0sdom1dom  9148  fineqvlem  9168  f1finf1o  9175  isfiniteg  9202  inficl  9330  tc00  9657  cardnueq0  9878  cardsdomel  9888  wdomfil  9973  wdomnumr  9976  alephsucdom  9991  cardalephex  10002  dfac12lem2  10057  cfeq0  10168  fin23lem24  10234  fin1a2lem9  10320  carden  10463  axrepnd  10507  axacndlem4  10523  gchpwdom  10583  gchina  10612  r1tskina  10695  addcanpi  10812  mulcanpi  10813  elnpi  10901  addcan  11319  addcan2  11320  neg11  11434  negreb  11448  add20  11651  mulcand  11772  cru  12139  nn0lt10b  12556  uz11  12778  eqreznegel  12849  lbzbi  12851  rpnnen1lem6  12897  xrmaxlt  13098  xrltmin  13099  xrmaxle  13100  xrlemin  13101  xneg11  13132  xnn0xadd0  13164  xsubge0  13178  xrub  13229  elioc2  13327  elico2  13328  elicc2  13329  fzopth  13479  2ffzeq  13567  fzoopth  13680  flidz  13732  addmodlteq  13871  expeq0  14017  sq01  14150  fz1eqb  14279  hashen1  14295  hash1snb  14344  hashle2pr  14402  wrdnval  14470  eqwrd  14482  ccatalpha  14519  wrdl1s1  14540  ccats1alpha  14545  ccatopth  14641  ccatopth2  14642  wrdlen2  14869  cj11  15087  sqrt0  15166  abs00  15214  recan  15262  cnsqrt00  15318  rlimdm  15476  rpnnen2lem12  16152  0dvds  16205  dvds1  16248  alzdvds  16249  nn0enne  16306  nn0oddm1d2  16314  nnoddm1d2  16315  gcdeq0  16446  algcvgblem  16506  2mulprm  16622  prmexpb  16648  prmreclem3  16848  4sqlem11  16885  moni  17662  chnfibg  18561  grprcan  18905  grplcan  18932  grpinv11  18939  grpinv11OLD  18940  galcan  19235  sylow2a  19550  subgdisjb  19624  0ringdif  20462  domnlcanb  20655  domnrcanb  20657  drngmuleq0  20698  fidomndrng  20708  lspsncmp  21073  xrsdsreclb  21370  znidomb  21518  lmisfree  21799  coe1tm  22217  tgdom  22924  en1top  22930  cmpfi  23354  txcmpb  23590  hmeocnvb  23720  flimcls  23931  hauspwpwf1  23933  flftg  23942  ghmcnp  24061  metrest  24470  icoopnst  24894  iocopnst  24895  ishl2  25328  vitali  25572  mbfi1fseqlem4  25677  aannenlem1  26294  perfect  27200  2lgsoddprmlem3  27383  2sq2  27402  ltsval2  27626  bday0b  27811  negs11  28047  elnns2  28339  n0cutlt  28357  umgrislfupgrlem  29197  usgrausgrb  29244  upgriswlk  29716  uhgrwkspth  29830  usgr2wlkspth  29834  usgr2trlspth  29836  usgr2pthspth  29837  extwwlkfab  30429  grporcan  30595  grpolcan  30607  ip2eqi  30933  hial2eq  31183  eigorthi  31914  stge1i  32315  stle0i  32316  mdbr3  32374  mdbr4  32375  atsseq  32424  mdsymlem7  32486  reuxfrdf  32567  disjunsn  32671  fpwrelmapffslem  32813  xmulcand  33004  prsdm  34073  prsrn  34074  lfuhgr  35314  lfuhgr2  35315  mthmpps  35778  untangtr  35910  filnetlem4  36577  ordtopconn  36635  ordtopt0  36638  bj-dfbi6  36777  bj-19.9htbi  36906  bj-elid6  37377  icorempo  37558  inunissunidif  37582  fvineqsneu  37618  wl-lem-moexsb  37775  seqpo  37950  lshpcmp  39270  lsatcmp  39285  lsatcmp2  39286  ltrneq2  40430  ltrneq  40431  tendospcanN  41305  dochlkr  41667  lcfl7N  41783  hgmap11  42184  ccatcan2d  42527  remulcan2d  42533  itrere  42594  log11d  42622  resubcan2  42664  readdcan2  42689  sn-addcand  42696  sn-addcan2d  42698  remulcand  42715  sn-itrere  42764  sn-retire  42765  cnreeu  42766  fphpd  43079  pellexlem3  43094  qirropth  43171  expdioph  43286  rpnnen3  43295  iotasbc  44681  f1ocof1ob2  47349  2reu3  47377  rlimdmafv  47444  afv2orxorb  47495  rlimdmafv2  47525  funop1  47550  2ffzoeq  47594  prprelprb  47784  poprelb  47791  evenprm2  47981  perfectALTV  47990  nnsum3primesle9  48061  upgrwlkupwlkb  48408  islinindfis  48716  lincresunit3lem3  48741  blen1b  48855  line2ylem  49018  line2y  49022  intubeu  49250  unilbeu  49251  thincn0eu  49697