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  2204  axc16gb  2262  equs5  2464  2eu1  2650  2eu1v  2651  2eu3  2653  ceqsalgALT  3497  eqvincg  3627  reuxfrd  3731  2reu1  3872  disjeq0  4431  undif4  4442  iftrueb  4513  ssprsseq  4801  sneqbg  4819  preq1b  4822  opthpr  4827  preq12nebg  4839  opthprneg  4841  dfiun2g  5006  elpwuni  5081  disjxiun  5116  eusv2i  5364  reusv2lem3  5370  reusv3  5375  soltmin  6125  ssxpb  6163  xp11  6164  xpcan  6165  xpcan2  6166  ordssun  6455  suc11  6460  unizlim  6476  imadif  6619  2elresin  6658  mpteqb  7004  f1fveq  7254  f1elima  7255  f1imass  7256  fliftf  7307  funeldmb  7351  sorpssuni  7724  sorpssint  7725  iunpw  7763  ssonprc  7779  onint0  7783  oa00  8569  omcan  8579  omopth2  8594  oecan  8599  nnarcl  8626  iserd  8743  mapfset  8862  map0g  8896  fundmen  9043  fopwdom  9092  onfin  9237  0sdom1dom  9244  fineqvlem  9268  f1finf1o  9275  f1finf1oOLD  9276  isfiniteg  9307  inficl  9435  tc00  9760  cardnueq0  9976  cardsdomel  9986  wdomfil  10073  wdomnumr  10076  alephsucdom  10091  cardalephex  10102  dfac12lem2  10157  cfeq0  10268  fin23lem24  10334  fin1a2lem9  10420  carden  10563  axrepnd  10606  axacndlem4  10622  gchpwdom  10682  gchina  10711  r1tskina  10794  addcanpi  10911  mulcanpi  10912  elnpi  11000  addcan  11417  addcan2  11418  neg11  11532  negreb  11546  add20  11747  mulcand  11868  cru  12230  nn0lt10b  12653  uz11  12875  eqreznegel  12948  lbzbi  12950  rpnnen1lem6  12996  xrmaxlt  13195  xrltmin  13196  xrmaxle  13197  xrlemin  13198  xneg11  13229  xnn0xadd0  13261  xsubge0  13275  xrub  13326  elioc2  13424  elico2  13425  elicc2  13426  fzopth  13576  2ffzeq  13664  fzoopth  13776  flidz  13825  addmodlteq  13962  expeq0  14108  sq01  14241  fz1eqb  14370  hashen1  14386  hash1snb  14435  hashle2pr  14493  wrdnval  14561  eqwrd  14573  ccatalpha  14609  wrdl1s1  14630  ccats1alpha  14635  ccatopth  14732  ccatopth2  14733  wrdlen2  14961  cj11  15179  sqrt0  15258  abs00  15306  recan  15353  cnsqrt00  15409  rlimdm  15565  rpnnen2lem12  16241  0dvds  16294  dvds1  16336  alzdvds  16337  nn0enne  16394  nn0oddm1d2  16402  nnoddm1d2  16403  gcdeq0  16534  algcvgblem  16594  2mulprm  16710  prmexpb  16736  prmreclem3  16936  4sqlem11  16973  moni  17747  grprcan  18954  grplcan  18981  grpinv11  18988  grpinv11OLD  18989  galcan  19285  sylow2a  19598  subgdisjb  19672  0ringdif  20485  domnlcanb  20678  domnrcanb  20680  drngmuleq0  20721  fidomndrng  20731  lspsncmp  21075  xrsdsreclb  21379  znidomb  21520  lmisfree  21800  coe1tm  22208  tgdom  22914  en1top  22920  cmpfi  23344  txcmpb  23580  hmeocnvb  23710  flimcls  23921  hauspwpwf1  23923  flftg  23932  ghmcnp  24051  metrest  24461  icoopnst  24885  iocopnst  24886  ishl2  25320  vitali  25564  mbfi1fseqlem4  25669  aannenlem1  26286  perfect  27192  2lgsoddprmlem3  27375  2sq2  27394  sltval2  27618  bday0b  27792  negs11  27998  elnns2  28261  umgrislfupgrlem  29047  usgrausgrb  29094  upgriswlk  29567  uhgrwkspth  29683  usgr2wlkspth  29687  usgr2trlspth  29689  usgr2pthspth  29690  extwwlkfab  30279  grporcan  30445  grpolcan  30457  ip2eqi  30783  hial2eq  31033  eigorthi  31764  stge1i  32165  stle0i  32166  mdbr3  32224  mdbr4  32225  atsseq  32274  mdsymlem7  32336  reuxfrdf  32418  disjunsn  32521  fpwrelmapffslem  32655  xmulcand  32841  prsdm  33891  prsrn  33892  lfuhgr  35086  lfuhgr2  35087  mthmpps  35550  untangtr  35677  filnetlem4  36345  ordtopconn  36403  ordtopt0  36406  bj-dfbi6  36539  bj-19.9htbi  36667  bj-elid6  37134  icorempo  37315  inunissunidif  37339  fvineqsneu  37375  wl-lem-moexsb  37532  seqpo  37717  lshpcmp  38952  lsatcmp  38967  lsatcmp2  38968  ltrneq2  40113  ltrneq  40114  tendospcanN  40988  dochlkr  41350  lcfl7N  41466  hgmap11  41867  ccatcan2d  42249  remulcan2d  42255  itrere  42314  log11d  42342  resubcan2  42378  readdcan2  42402  sn-addcand  42409  sn-addcan2d  42411  remulcand  42428  sn-itrere  42458  sn-retire  42459  cnreeu  42460  fphpd  42786  pellexlem3  42801  qirropth  42878  expdioph  42994  rpnnen3  43003  iotasbc  44391  f1ocof1ob2  47059  2reu3  47087  rlimdmafv  47154  afv2orxorb  47205  rlimdmafv2  47235  funop1  47260  2ffzoeq  47304  prprelprb  47479  poprelb  47486  evenprm2  47676  perfectALTV  47685  nnsum3primesle9  47756  upgrwlkupwlkb  48064  islinindfis  48373  lincresunit3lem3  48398  blen1b  48516  line2ylem  48679  line2y  48683  intubeu  48906  unilbeu  48907  thincn0eu  49265