Theorem sylanl1 678

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 396

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 206  df-an 397

This theorem is referenced by:  adantlll  716  adantllr  717  adantl3r  748  isocnv  7329  f1iun  7932  odi  8581  oeoelem  8600  mapxpen  9145  xadddilem  13277  hashgt23el  14388  pcqmul  16790  infpnlem1  16847  setsn0fun  17110  chpdmat  22563  neitr  22904  hausflimi  23704  nmoix  24466  nmoleub  24468  metdsre  24589  bncssbn  25115  usgr2edg  28722  usgr2edg1  28724  crctcshwlkn0  29330  unoplin  31428  hmoplin  31450  chirredlem1  31898  mdsymlem2  31912  foresf1o  31997  zarcls1  33135  ordtconnlem1  33190  signstfvn  33866  isbasisrelowllem1  36539  isbasisrelowllem2  36540  pibt2  36601  lindsadd  36784  lindsdom  36785  matunitlindflem1  36787  matunitlindflem2  36788  poimirlem25  36816  poimirlem29  36820  heicant  36826  cnambfre  36839  itg2addnclem  36842  ftc1anclem5  36868  ftc1anc  36872  rrnequiv  37006  isfldidl  37239  ispridlc  37241  supxrgelem  44346  supminfxr  44473  itcovalt2lem2  47450  reccot  47891  rectan  47892