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  1618  19.33b  1885  19.40b  1888  19.9t  2205  axc16gb  2263  equs5  2459  2eu1  2645  2eu1v  2646  2eu3  2648  ceqsalgALT  3487  eqvincg  3617  reuxfrd  3722  2reu1  3863  disjeq0  4422  undif4  4433  iftrueb  4504  ssprsseq  4792  sneqbg  4810  preq1b  4813  opthpr  4818  preq12nebg  4830  opthprneg  4832  dfiun2g  4997  elpwuni  5072  disjxiun  5107  eusv2i  5352  reusv2lem3  5358  reusv3  5363  soltmin  6112  ssxpb  6150  xp11  6151  xpcan  6152  xpcan2  6153  ordssun  6439  suc11  6444  unizlim  6460  imadif  6603  2elresin  6642  mpteqb  6990  f1fveq  7240  f1elima  7241  f1imass  7242  fliftf  7293  funeldmb  7337  sorpssuni  7711  sorpssint  7712  iunpw  7750  ssonprc  7766  onint0  7770  oa00  8526  omcan  8536  omopth2  8551  oecan  8556  nnarcl  8583  iserd  8700  mapfset  8826  map0g  8860  fundmen  9005  fopwdom  9054  onfin  9185  0sdom1dom  9192  fineqvlem  9216  f1finf1o  9223  f1finf1oOLD  9224  isfiniteg  9255  inficl  9383  tc00  9708  cardnueq0  9924  cardsdomel  9934  wdomfil  10021  wdomnumr  10024  alephsucdom  10039  cardalephex  10050  dfac12lem2  10105  cfeq0  10216  fin23lem24  10282  fin1a2lem9  10368  carden  10511  axrepnd  10554  axacndlem4  10570  gchpwdom  10630  gchina  10659  r1tskina  10742  addcanpi  10859  mulcanpi  10860  elnpi  10948  addcan  11365  addcan2  11366  neg11  11480  negreb  11494  add20  11697  mulcand  11818  cru  12185  nn0lt10b  12603  uz11  12825  eqreznegel  12900  lbzbi  12902  rpnnen1lem6  12948  xrmaxlt  13148  xrltmin  13149  xrmaxle  13150  xrlemin  13151  xneg11  13182  xnn0xadd0  13214  xsubge0  13228  xrub  13279  elioc2  13377  elico2  13378  elicc2  13379  fzopth  13529  2ffzeq  13617  fzoopth  13730  flidz  13779  addmodlteq  13918  expeq0  14064  sq01  14197  fz1eqb  14326  hashen1  14342  hash1snb  14391  hashle2pr  14449  wrdnval  14517  eqwrd  14529  ccatalpha  14565  wrdl1s1  14586  ccats1alpha  14591  ccatopth  14688  ccatopth2  14689  wrdlen2  14917  cj11  15135  sqrt0  15214  abs00  15262  recan  15310  cnsqrt00  15366  rlimdm  15524  rpnnen2lem12  16200  0dvds  16253  dvds1  16296  alzdvds  16297  nn0enne  16354  nn0oddm1d2  16362  nnoddm1d2  16363  gcdeq0  16494  algcvgblem  16554  2mulprm  16670  prmexpb  16696  prmreclem3  16896  4sqlem11  16933  moni  17705  grprcan  18912  grplcan  18939  grpinv11  18946  grpinv11OLD  18947  galcan  19243  sylow2a  19556  subgdisjb  19630  0ringdif  20443  domnlcanb  20636  domnrcanb  20638  drngmuleq0  20679  fidomndrng  20689  lspsncmp  21033  xrsdsreclb  21337  znidomb  21478  lmisfree  21758  coe1tm  22166  tgdom  22872  en1top  22878  cmpfi  23302  txcmpb  23538  hmeocnvb  23668  flimcls  23879  hauspwpwf1  23881  flftg  23890  ghmcnp  24009  metrest  24419  icoopnst  24843  iocopnst  24844  ishl2  25277  vitali  25521  mbfi1fseqlem4  25626  aannenlem1  26243  perfect  27149  2lgsoddprmlem3  27332  2sq2  27351  sltval2  27575  bday0b  27749  negs11  27962  elnns2  28240  n0cutlt  28256  umgrislfupgrlem  29056  usgrausgrb  29103  upgriswlk  29576  uhgrwkspth  29692  usgr2wlkspth  29696  usgr2trlspth  29698  usgr2pthspth  29699  extwwlkfab  30288  grporcan  30454  grpolcan  30466  ip2eqi  30792  hial2eq  31042  eigorthi  31773  stge1i  32174  stle0i  32175  mdbr3  32233  mdbr4  32234  atsseq  32283  mdsymlem7  32345  reuxfrdf  32427  disjunsn  32530  fpwrelmapffslem  32662  xmulcand  32848  prsdm  33911  prsrn  33912  lfuhgr  35112  lfuhgr2  35113  mthmpps  35576  untangtr  35708  filnetlem4  36376  ordtopconn  36434  ordtopt0  36437  bj-dfbi6  36570  bj-19.9htbi  36698  bj-elid6  37165  icorempo  37346  inunissunidif  37370  fvineqsneu  37406  wl-lem-moexsb  37563  seqpo  37748  lshpcmp  38988  lsatcmp  39003  lsatcmp2  39004  ltrneq2  40149  ltrneq  40150  tendospcanN  41024  dochlkr  41386  lcfl7N  41502  hgmap11  41903  ccatcan2d  42246  remulcan2d  42252  itrere  42313  log11d  42341  resubcan2  42383  readdcan2  42408  sn-addcand  42415  sn-addcan2d  42417  remulcand  42434  sn-itrere  42483  sn-retire  42484  cnreeu  42485  fphpd  42811  pellexlem3  42826  qirropth  42903  expdioph  43019  rpnnen3  43028  iotasbc  44415  f1ocof1ob2  47087  2reu3  47115  rlimdmafv  47182  afv2orxorb  47233  rlimdmafv2  47263  funop1  47288  2ffzoeq  47332  prprelprb  47522  poprelb  47529  evenprm2  47719  perfectALTV  47728  nnsum3primesle9  47799  upgrwlkupwlkb  48133  islinindfis  48442  lincresunit3lem3  48467  blen1b  48581  line2ylem  48744  line2y  48748  intubeu  48976  unilbeu  48977  thincn0eu  49424