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  7259  f1iun  7871  odi  8489  oeoelem  8508  mapxpen  9051  xadddilem  13185  hashgt23el  14323  pcqmul  16757  infpnlem1  16814  setsn0fun  17076  chpdmat  22749  neitr  23088  hausflimi  23888  nmoix  24637  nmoleub  24639  metdsre  24762  bncssbn  25294  usgr2edg  29181  usgr2edg1  29183  crctcshwlkn0  29792  unoplin  31890  hmoplin  31912  chirredlem1  32360  mdsymlem2  32374  foresf1o  32474  zarcls1  33872  ordtconnlem1  33927  signstfvn  34572  isbasisrelowllem1  37368  isbasisrelowllem2  37369  pibt2  37430  lindsadd  37632  lindsdom  37633  matunitlindflem1  37635  matunitlindflem2  37636  poimirlem25  37664  poimirlem29  37668  heicant  37674  cnambfre  37687  itg2addnclem  37690  ftc1anclem5  37716  ftc1anc  37720  rrnequiv  37854  isfldidl  38087  ispridlc  38089  supxrgelem  45355  supminfxr  45481  uhgrimisgrgric  47941  cycl3grtri  47957  gpg5nbgrvtx03star  48090  gpg5nbgr3star  48091  itcovalt2lem2  48687  reccot  49769  rectan  49770