Theorem biimp3a 1465

Description: Infer implication from a logical equivalence. Similar to biimpa 479. (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 479	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	2	3impa 1106	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  nn0addge1  11937  nn0addge2  11938  nn0sub2  12037  eluzp1p1  12264  uznn0sub  12271  uzinfi  12322  iocssre  12810  icossre  12811  iccssre  12812  lincmb01cmp  12875  iccf1o  12876  fzosplitprm1  13141  subfzo0  13153  modfzo0difsn  13305  hashprb  13752  pfxpfx  14064  eflt  15464  fldivndvdslt  15759  prmdiv  16116  hashgcdlem  16119  vfermltl  16132  coprimeprodsq  16139  pythagtrip  16165  difsqpwdvds  16217  cshwshashlem2  16424  odinf  18684  odcl2  18686  slesolex  21285  tgtop11  21584  restntr  21784  hauscmplem  22008  icchmeo  23539  pi1xfr  23653  sinq12gt0  25087  tanord1  25115  gausslemma2dlem1a  25935  axsegconlem6  26702  lfuhgr1v0e  27030  crctcshwlkn0lem6  27587  crctcshwlkn0lem7  27588  clwlkclwwlkf1lem2  27777  s2elclwwlknon2  27877  eucrctshift  28016  eucrct2eupth  28018  nv1  28446  lnolin  28525  br8d  30355  fzm1ne1  30506  cycpmco2lem6  30768  ballotlemfc0  31745  ballotlemfcc  31746  ballotlemrv2  31774  fisshasheq  32347  br8  32987  br6  32988  br4  32989  ismtyima  35075  ismtybndlem  35078  ghomlinOLD  35160  ghomidOLD  35161  cvrcmp2  36414  atcvrj2  36563  1cvratex  36603  lplnric  36682  lplnri1  36683  lnatexN  36909  ltrnateq  37311  ltrnatneq  37312  cdleme46f2g2  37623  cdleme46f2g1  37624  dibelval1st  38279  dibelval2nd  38282  dicelval1sta  38317  hlhilphllem  39089  jm2.17b  39551  bi123impia  40816  sineq0ALT  41264  eliccre  41773  ioomidp  41782  smfinflem  43084  iccpartiltu  43575  goldbachthlem1  43700  evengpop3  43956  rnghmresel  44228  rhmresel  44274