Theorem sylanl1 686

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 621	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 586	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 208  df-an 397

This theorem is referenced by:  adantlll  724  adantllr  725  adantl3r  756  isocnv  7281  f1iun  7893  odi  8511  oeoelem  8531  mapxpen  9078  xadddilem  13244  hashgt23el  14384  pcqmul  16822  infpnlem1  16879  setsn0fun  17141  chpdmat  22831  neitr  23170  hausflimi  23970  nmoix  24719  nmoleub  24721  metdsre  24844  bncssbn  25366  usgr2edg  29304  usgr2edg1  29306  crctcshwlkn0  29914  unoplin  32016  hmoplin  32038  chirredlem1  32486  mdsymlem2  32500  foresf1o  32599  zarcls1  34060  ordtconnlem1  34115  signstfvn  34760  isbasisrelowllem1  37724  isbasisrelowllem2  37725  pibt2  37786  lindsadd  37987  lindsdom  37988  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem25  38019  poimirlem29  38023  heicant  38029  cnambfre  38042  itg2addnclem  38045  ftc1anclem5  38071  ftc1anc  38075  rrnequiv  38209  isfldidl  38442  ispridlc  38444  supxrgelem  45789  supminfxr  45914  uhgrimisgrgric  48429  cycl3grtri  48445  gpg5nbgrvtx03star  48578  gpg5nbgr3star  48579  itcovalt2lem2  49174  reccot  50255  rectan  50256