Theorem sylanl1 680

Description: A syllogism inference. (Contributed by NM, 10-Mar-2005.)

Hypotheses

Ref	Expression
sylanl1.1	⊢ (𝜑 → 𝜓)
sylanl1.2	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
sylanl1	⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem sylanl1

Step	Hyp	Ref	Expression
1		sylanl1.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	anim1i 615	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 580	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395

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  df-an 396

This theorem is referenced by:  adantlll  718  adantllr  719  adantl3r  750  isocnv  7270  f1iun  7882  odi  8500  oeoelem  8519  mapxpen  9063  xadddilem  13195  hashgt23el  14333  pcqmul  16767  infpnlem1  16824  setsn0fun  17086  chpdmat  22757  neitr  23096  hausflimi  23896  nmoix  24645  nmoleub  24647  metdsre  24770  bncssbn  25302  usgr2edg  29190  usgr2edg1  29192  crctcshwlkn0  29801  unoplin  31902  hmoplin  31924  chirredlem1  32372  mdsymlem2  32386  foresf1o  32486  zarcls1  33903  ordtconnlem1  33958  signstfvn  34603  isbasisrelowllem1  37420  isbasisrelowllem2  37421  pibt2  37482  lindsadd  37674  lindsdom  37675  matunitlindflem1  37677  matunitlindflem2  37678  poimirlem25  37706  poimirlem29  37710  heicant  37716  cnambfre  37729  itg2addnclem  37732  ftc1anclem5  37758  ftc1anc  37762  rrnequiv  37896  isfldidl  38129  ispridlc  38131  supxrgelem  45461  supminfxr  45587  uhgrimisgrgric  48056  cycl3grtri  48072  gpg5nbgrvtx03star  48205  gpg5nbgr3star  48206  itcovalt2lem2  48802  reccot  49884  rectan  49885