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  1001  pm5.71  1028  cad0  1615  cad0OLD  1616  19.33b  1884  19.40b  1887  19.9t  2205  axc16gb  2263  equs5  2468  2eu1  2654  2eu1v  2655  2eu3  2657  ceqsalgALT  3526  eqvincg  3661  reuxfrd  3770  2reu1  3919  disjeq0  4479  undif4  4490  ssprsseq  4850  sneqbg  4868  preq1b  4871  opthpr  4876  preq12nebg  4887  opthprneg  4889  dfiun2g  5053  elpwuni  5128  disjxiun  5163  eusv2i  5412  reusv2lem3  5418  reusv3  5423  soltmin  6168  ssxpb  6205  xp11  6206  xpcan  6207  xpcan2  6208  ordssun  6497  suc11  6502  unizlim  6518  imadif  6662  2elresin  6701  mpteqb  7048  f1fveq  7299  f1elima  7300  f1imass  7301  fliftf  7351  funeldmb  7395  sorpssuni  7767  sorpssint  7768  iunpw  7806  ssonprc  7823  onint0  7827  oa00  8615  omcan  8625  omopth2  8640  oecan  8645  nnarcl  8672  iserd  8789  mapfset  8908  map0g  8942  fundmen  9096  fopwdom  9146  onfin  9293  0sdom1dom  9301  fineqvlem  9325  f1finf1o  9333  f1finf1oOLD  9334  isfiniteg  9365  inficl  9494  tc00  9817  cardnueq0  10033  cardsdomel  10043  wdomfil  10130  wdomnumr  10133  alephsucdom  10148  cardalephex  10159  dfac12lem2  10214  cfeq0  10325  fin23lem24  10391  fin1a2lem9  10477  carden  10620  axrepnd  10663  axacndlem4  10679  gchpwdom  10739  gchina  10768  r1tskina  10851  addcanpi  10968  mulcanpi  10969  elnpi  11057  addcan  11474  addcan2  11475  neg11  11587  negreb  11601  add20  11802  mulcand  11923  cru  12285  nn0lt10b  12705  uz11  12928  eqreznegel  12999  lbzbi  13001  rpnnen1lem6  13047  xrmaxlt  13243  xrltmin  13244  xrmaxle  13245  xrlemin  13246  xneg11  13277  xnn0xadd0  13309  xsubge0  13323  xrub  13374  elioc2  13470  elico2  13471  elicc2  13472  fzopth  13621  2ffzeq  13706  fzoopth  13812  flidz  13861  addmodlteq  13997  expeq0  14143  sq01  14274  fz1eqb  14403  hashen1  14419  hash1snb  14468  hashle2pr  14526  wrdnval  14593  eqwrd  14605  ccatalpha  14641  wrdl1s1  14662  ccats1alpha  14667  ccatopth  14764  ccatopth2  14765  wrdlen2  14993  cj11  15211  sqrt0  15290  abs00  15338  recan  15385  cnsqrt00  15441  rlimdm  15597  rpnnen2lem12  16273  0dvds  16325  dvds1  16367  alzdvds  16368  nn0enne  16425  nn0oddm1d2  16433  nnoddm1d2  16434  gcdeq0  16563  algcvgblem  16624  2mulprm  16740  prmexpb  16766  prmreclem3  16965  4sqlem11  17002  moni  17797  grprcan  19013  grplcan  19040  grpinv11  19047  grpinv11OLD  19048  galcan  19344  sylow2a  19661  subgdisjb  19735  0ringdif  20553  domnlcanb  20742  domnrcanb  20744  drngmuleq0  20785  fidomndrng  20796  lspsncmp  21141  xrsdsreclb  21454  znidomb  21603  lmisfree  21885  coe1tm  22297  tgdom  23006  en1top  23012  cmpfi  23437  txcmpb  23673  hmeocnvb  23803  flimcls  24014  hauspwpwf1  24016  flftg  24025  ghmcnp  24144  metrest  24558  icoopnst  24988  iocopnst  24989  ishl2  25423  vitali  25667  mbfi1fseqlem4  25773  aannenlem1  26388  perfect  27293  2lgsoddprmlem3  27476  2sq2  27495  sltval2  27719  bday0b  27893  negs11  28099  elnns2  28362  umgrislfupgrlem  29157  usgrausgrb  29204  upgriswlk  29677  uhgrwkspth  29791  usgr2wlkspth  29795  usgr2trlspth  29797  usgr2pthspth  29798  extwwlkfab  30384  grporcan  30550  grpolcan  30562  ip2eqi  30888  hial2eq  31138  eigorthi  31869  stge1i  32270  stle0i  32271  mdbr3  32329  mdbr4  32330  atsseq  32379  mdsymlem7  32441  reuxfrdf  32519  disjunsn  32616  fpwrelmapffslem  32746  xmulcand  32885  prsdm  33860  prsrn  33861  lfuhgr  35085  lfuhgr2  35086  mthmpps  35550  untangtr  35676  filnetlem4  36347  ordtopconn  36405  ordtopt0  36408  bj-dfbi6  36541  bj-19.9htbi  36669  bj-elid6  37136  icorempo  37317  inunissunidif  37341  fvineqsneu  37377  wl-lem-moexsb  37522  seqpo  37707  lshpcmp  38944  lsatcmp  38959  lsatcmp2  38960  ltrneq2  40105  ltrneq  40106  tendospcanN  40980  dochlkr  41342  lcfl7N  41458  hgmap11  41859  ccatcan2d  42246  remulcan2d  42252  itrere  42307  log11d  42334  resubcan2  42364  readdcan2  42388  sn-addcand  42395  sn-addcan2d  42397  remulcand  42414  sn-itrere  42444  sn-retire  42445  cnreeu  42446  fphpd  42772  pellexlem3  42787  qirropth  42864  expdioph  42980  rpnnen3  42989  iotasbc  44388  f1ocof1ob2  46997  2reu3  47025  rlimdmafv  47092  afv2orxorb  47143  rlimdmafv2  47173  funop1  47198  2ffzoeq  47242  prprelprb  47391  poprelb  47398  evenprm2  47588  perfectALTV  47597  nnsum3primesle9  47668  upgrwlkupwlkb  47864  islinindfis  48178  lincresunit3lem3  48203  blen1b  48322  line2ylem  48485  line2y  48489  intubeu  48656  unilbeu  48657  thincn0eu  48699