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  2458  2eu1  2644  2eu1v  2645  2eu3  2647  ceqsalgALT  3473  eqvincg  3603  reuxfrd  3708  2reu1  3849  disjeq0  4407  undif4  4418  iftrueb  4489  ssprsseq  4776  sneqbg  4794  preq1b  4797  opthpr  4802  preq12nebg  4814  opthprneg  4816  dfiun2g  4980  elpwuni  5054  disjxiun  5089  eusv2i  5333  reusv2lem3  5339  reusv3  5344  soltmin  6085  ssxpb  6123  xp11  6124  xpcan  6125  xpcan2  6126  ordssun  6411  suc11  6416  unizlim  6431  imadif  6566  2elresin  6603  mpteqb  6949  f1fveq  7199  f1elima  7200  f1imass  7201  fliftf  7252  funeldmb  7296  sorpssuni  7668  sorpssint  7669  iunpw  7707  ssonprc  7723  onint0  7727  oa00  8477  omcan  8487  omopth2  8502  oecan  8507  nnarcl  8534  iserd  8651  mapfset  8777  map0g  8811  fundmen  8956  fopwdom  9002  onfin  9129  0sdom1dom  9135  fineqvlem  9155  f1finf1o  9162  isfiniteg  9189  inficl  9315  tc00  9644  cardnueq0  9860  cardsdomel  9870  wdomfil  9955  wdomnumr  9958  alephsucdom  9973  cardalephex  9984  dfac12lem2  10039  cfeq0  10150  fin23lem24  10216  fin1a2lem9  10302  carden  10445  axrepnd  10488  axacndlem4  10504  gchpwdom  10564  gchina  10593  r1tskina  10676  addcanpi  10793  mulcanpi  10794  elnpi  10882  addcan  11300  addcan2  11301  neg11  11415  negreb  11429  add20  11632  mulcand  11753  cru  12120  nn0lt10b  12538  uz11  12760  eqreznegel  12835  lbzbi  12837  rpnnen1lem6  12883  xrmaxlt  13083  xrltmin  13084  xrmaxle  13085  xrlemin  13086  xneg11  13117  xnn0xadd0  13149  xsubge0  13163  xrub  13214  elioc2  13312  elico2  13313  elicc2  13314  fzopth  13464  2ffzeq  13552  fzoopth  13665  flidz  13714  addmodlteq  13853  expeq0  13999  sq01  14132  fz1eqb  14261  hashen1  14277  hash1snb  14326  hashle2pr  14384  wrdnval  14452  eqwrd  14464  ccatalpha  14500  wrdl1s1  14521  ccats1alpha  14526  ccatopth  14622  ccatopth2  14623  wrdlen2  14851  cj11  15069  sqrt0  15148  abs00  15196  recan  15244  cnsqrt00  15300  rlimdm  15458  rpnnen2lem12  16134  0dvds  16187  dvds1  16230  alzdvds  16231  nn0enne  16288  nn0oddm1d2  16296  nnoddm1d2  16297  gcdeq0  16428  algcvgblem  16488  2mulprm  16604  prmexpb  16630  prmreclem3  16830  4sqlem11  16867  moni  17643  grprcan  18852  grplcan  18879  grpinv11  18886  grpinv11OLD  18887  galcan  19183  sylow2a  19498  subgdisjb  19572  0ringdif  20412  domnlcanb  20605  domnrcanb  20607  drngmuleq0  20648  fidomndrng  20658  lspsncmp  21023  xrsdsreclb  21320  znidomb  21468  lmisfree  21749  coe1tm  22157  tgdom  22863  en1top  22869  cmpfi  23293  txcmpb  23529  hmeocnvb  23659  flimcls  23870  hauspwpwf1  23872  flftg  23881  ghmcnp  24000  metrest  24410  icoopnst  24834  iocopnst  24835  ishl2  25268  vitali  25512  mbfi1fseqlem4  25617  aannenlem1  26234  perfect  27140  2lgsoddprmlem3  27323  2sq2  27342  sltval2  27566  bday0b  27744  negs11  27960  elnns2  28238  n0cutlt  28254  umgrislfupgrlem  29067  usgrausgrb  29114  upgriswlk  29586  uhgrwkspth  29700  usgr2wlkspth  29704  usgr2trlspth  29706  usgr2pthspth  29707  extwwlkfab  30296  grporcan  30462  grpolcan  30474  ip2eqi  30800  hial2eq  31050  eigorthi  31781  stge1i  32182  stle0i  32183  mdbr3  32241  mdbr4  32242  atsseq  32291  mdsymlem7  32353  reuxfrdf  32435  disjunsn  32538  fpwrelmapffslem  32676  xmulcand  32862  prsdm  33887  prsrn  33888  lfuhgr  35101  lfuhgr2  35102  mthmpps  35565  untangtr  35697  filnetlem4  36365  ordtopconn  36423  ordtopt0  36426  bj-dfbi6  36559  bj-19.9htbi  36687  bj-elid6  37154  icorempo  37335  inunissunidif  37359  fvineqsneu  37395  wl-lem-moexsb  37552  seqpo  37737  lshpcmp  38977  lsatcmp  38992  lsatcmp2  38993  ltrneq2  40137  ltrneq  40138  tendospcanN  41012  dochlkr  41374  lcfl7N  41490  hgmap11  41891  ccatcan2d  42234  remulcan2d  42240  itrere  42301  log11d  42329  resubcan2  42371  readdcan2  42396  sn-addcand  42403  sn-addcan2d  42405  remulcand  42422  sn-itrere  42471  sn-retire  42472  cnreeu  42473  fphpd  42799  pellexlem3  42814  qirropth  42891  expdioph  43006  rpnnen3  43015  iotasbc  44402  f1ocof1ob2  47076  2reu3  47104  rlimdmafv  47171  afv2orxorb  47222  rlimdmafv2  47252  funop1  47277  2ffzoeq  47321  prprelprb  47511  poprelb  47518  evenprm2  47708  perfectALTV  47717  nnsum3primesle9  47788  upgrwlkupwlkb  48135  islinindfis  48444  lincresunit3lem3  48469  blen1b  48583  line2ylem  48746  line2y  48750  intubeu  48978  unilbeu  48979  thincn0eu  49426