Theorem biimp3a 1461

Description: Infer implication from a logical equivalence. Similar to biimpa 477. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
biimp3a.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
biimp3a	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem biimp3a

Step	Hyp	Ref	Expression
1		biimp3a.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	biimpa 477	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1103	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  nn0addge1  11793  nn0addge2  11794  nn0sub2  11893  eluzp1p1  12119  uznn0sub  12126  uzinfi  12177  iocssre  12666  icossre  12667  iccssre  12668  lincmb01cmp  12731  iccf1o  12732  fzosplitprm1  12997  subfzo0  13009  modfzo0difsn  13161  hashprb  13606  pfxpfx  13906  repswpfx  13983  eflt  15303  fldivndvdslt  15598  prmdiv  15951  hashgcdlem  15954  vfermltl  15967  coprimeprodsq  15974  pythagtrip  16000  difsqpwdvds  16052  cshwshashlem2  16259  odinf  18420  odcl2  18422  slesolex  20975  tgtop11  21274  restntr  21474  hauscmplem  21698  icchmeo  23228  pi1xfr  23342  sinq12gt0  24776  tanord1  24802  gausslemma2dlem1a  25623  axsegconlem6  26391  lfuhgr1v0e  26719  crctcshwlkn0lem6  27275  crctcshwlkn0lem7  27276  clwlkclwwlkf1lem2  27465  s2elclwwlknon2  27565  eucrctshift  27704  eucrct2eupth  27706  nv1  28135  lnolin  28214  br8d  30043  ballotlemfc0  31359  ballotlemfcc  31360  ballotlemrv2  31388  fisshasheq  31958  br8  32594  br6  32595  br4  32596  ismtyima  34626  ismtybndlem  34629  ghomlinOLD  34711  ghomidOLD  34712  cvrcmp2  35964  atcvrj2  36113  1cvratex  36153  lplnric  36232  lplnri1  36233  lnatexN  36459  ltrnateq  36861  ltrnatneq  36862  cdleme46f2g2  37173  cdleme46f2g1  37174  dibelval1st  37829  dibelval2nd  37832  dicelval1sta  37867  hlhilphllem  38639  jm2.17b  39056  bi123impia  40375  sineq0ALT  40823  eliccre  41336  ioomidp  41345  smfinflem  42647  iccpartiltu  43078  goldbachthlem1  43203  evengpop3  43459  rnghmresel  43727  rhmresel  43773