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  1003  pm5.71  1030  cad0  1620  19.33b  1887  19.40b  1890  19.9t  2212  axc16gb  2270  equs5  2464  2eu1  2651  2eu1v  2652  2eu3  2654  ceqsalgALT  3466  eqvincg  3590  reuxfrd  3694  2reu1  3835  disjeq0  4396  undif4  4407  iftrueb  4479  ssprsseq  4768  sneqbg  4786  preq1b  4789  opthpr  4794  preq12nebg  4806  opthprneg  4808  dfiun2g  4972  elpwuni  5047  disjxiun  5082  eusv2i  5336  reusv2lem3  5342  reusv3  5347  soltmin  6099  ssxpb  6138  xp11  6139  xpcan  6140  xpcan2  6141  ordssun  6427  suc11  6432  unizlim  6447  imadif  6582  2elresin  6619  mpteqb  6967  f1fveq  7217  f1elima  7218  f1imass  7219  fliftf  7270  funeldmb  7314  sorpssuni  7686  sorpssint  7687  iunpw  7725  ssonprc  7741  onint0  7745  oa00  8494  omcan  8504  omopth2  8519  oecan  8525  nnarcl  8552  iserd  8670  mapfset  8797  map0g  8832  fundmen  8978  fopwdom  9023  onfin  9149  0sdom1dom  9156  fineqvlem  9176  f1finf1o  9183  isfiniteg  9210  inficl  9338  tc00  9667  cardnueq0  9888  cardsdomel  9898  wdomfil  9983  wdomnumr  9986  alephsucdom  10001  cardalephex  10012  dfac12lem2  10067  cfeq0  10178  fin23lem24  10244  fin1a2lem9  10330  carden  10473  axrepnd  10517  axacndlem4  10533  gchpwdom  10593  gchina  10622  r1tskina  10705  addcanpi  10822  mulcanpi  10823  elnpi  10911  addcan  11330  addcan2  11331  neg11  11445  negreb  11459  add20  11662  mulcand  11783  cru  12151  nn0lt10b  12591  uz11  12813  eqreznegel  12884  lbzbi  12886  rpnnen1lem6  12932  xrmaxlt  13133  xrltmin  13134  xrmaxle  13135  xrlemin  13136  xneg11  13167  xnn0xadd0  13199  xsubge0  13213  xrub  13264  elioc2  13362  elico2  13363  elicc2  13364  fzopth  13515  2ffzeq  13603  fzoopth  13717  flidz  13769  addmodlteq  13908  expeq0  14054  sq01  14187  fz1eqb  14316  hashen1  14332  hash1snb  14381  hashle2pr  14439  wrdnval  14507  eqwrd  14519  ccatalpha  14556  wrdl1s1  14577  ccats1alpha  14582  ccatopth  14678  ccatopth2  14679  wrdlen2  14906  cj11  15124  sqrt0  15203  abs00  15251  recan  15299  cnsqrt00  15355  rlimdm  15513  rpnnen2lem12  16192  0dvds  16245  dvds1  16288  alzdvds  16289  nn0enne  16346  nn0oddm1d2  16354  nnoddm1d2  16355  gcdeq0  16486  algcvgblem  16546  2mulprm  16662  prmexpb  16689  prmreclem3  16889  4sqlem11  16926  moni  17703  chnfibg  18602  grprcan  18949  grplcan  18976  grpinv11  18983  grpinv11OLD  18984  galcan  19279  sylow2a  19594  subgdisjb  19668  0ringdif  20504  domnlcanb  20697  domnrcanb  20699  drngmuleq0  20740  fidomndrng  20750  lspsncmp  21114  xrsdsreclb  21394  znidomb  21541  lmisfree  21822  coe1tm  22238  tgdom  22943  en1top  22949  cmpfi  23373  txcmpb  23609  hmeocnvb  23739  flimcls  23950  hauspwpwf1  23952  flftg  23961  ghmcnp  24080  metrest  24489  icoopnst  24906  iocopnst  24907  ishl2  25337  vitali  25580  mbfi1fseqlem4  25685  aannenlem1  26294  perfect  27194  2lgsoddprmlem3  27377  2sq2  27396  ltsval2  27620  bday0b  27805  negs11  28041  elnns2  28333  n0cutlt  28351  umgrislfupgrlem  29191  usgrausgrb  29238  upgriswlk  29709  uhgrwkspth  29823  usgr2wlkspth  29827  usgr2trlspth  29829  usgr2pthspth  29830  extwwlkfab  30422  grporcan  30589  grpolcan  30601  ip2eqi  30927  hial2eq  31177  eigorthi  31908  stge1i  32309  stle0i  32310  mdbr3  32368  mdbr4  32369  atsseq  32418  mdsymlem7  32480  reuxfrdf  32560  disjunsn  32664  fpwrelmapffslem  32805  xmulcand  32980  prsdm  34058  prsrn  34059  lfuhgr  35300  lfuhgr2  35301  mthmpps  35764  untangtr  35896  filnetlem4  36563  ordtopconn  36621  ordtopt0  36624  bj-dfbi6  36840  bj-spvew  36930  bj-19.9htbi  37000  bj-axseprep  37381  bj-elid6  37484  icorempo  37667  inunissunidif  37691  fvineqsneu  37727  wl-lem-moexsb  37893  seqpo  38068  qmapeldisjsbi  39182  lshpcmp  39434  lsatcmp  39449  lsatcmp2  39450  ltrneq2  40594  ltrneq  40595  tendospcanN  41469  dochlkr  41831  lcfl7N  41947  hgmap11  42348  ccatcan2d  42690  remulcan2d  42695  itrere  42750  log11d  42778  resubcan2  42820  readdcan2  42845  sn-addcand  42852  sn-addcan2d  42854  remulcand  42871  sn-itrere  42933  sn-retire  42934  cnreeu  42935  fphpd  43244  pellexlem3  43259  qirropth  43336  expdioph  43451  rpnnen3  43460  iotasbc  44846  f1ocof1ob2  47530  2reu3  47558  rlimdmafv  47625  afv2orxorb  47676  rlimdmafv2  47706  funop1  47731  2ffzoeq  47776  prprelprb  47977  poprelb  47984  evenprm2  48190  perfectALTV  48199  nnsum3primesle9  48270  upgrwlkupwlkb  48617  islinindfis  48925  lincresunit3lem3  48950  blen1b  49064  line2ylem  49227  line2y  49231  intubeu  49459  unilbeu  49460  thincn0eu  49906