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  7276  f1iun  7888  odi  8506  oeoelem  8526  mapxpen  9071  xadddilem  13209  hashgt23el  14347  pcqmul  16781  infpnlem1  16838  setsn0fun  17100  chpdmat  22785  neitr  23124  hausflimi  23924  nmoix  24673  nmoleub  24675  metdsre  24798  bncssbn  25330  usgr2edg  29283  usgr2edg1  29285  crctcshwlkn0  29894  unoplin  31995  hmoplin  32017  chirredlem1  32465  mdsymlem2  32479  foresf1o  32579  zarcls1  34026  ordtconnlem1  34081  signstfvn  34726  isbasisrelowllem1  37556  isbasisrelowllem2  37557  pibt2  37618  lindsadd  37810  lindsdom  37811  matunitlindflem1  37813  matunitlindflem2  37814  poimirlem25  37842  poimirlem29  37846  heicant  37852  cnambfre  37865  itg2addnclem  37868  ftc1anclem5  37894  ftc1anc  37898  rrnequiv  38032  isfldidl  38265  ispridlc  38267  supxrgelem  45578  supminfxr  45704  uhgrimisgrgric  48173  cycl3grtri  48189  gpg5nbgrvtx03star  48322  gpg5nbgr3star  48323  itcovalt2lem2  48918  reccot  49999  rectan  50000