Theorem sylanl1 692

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 626	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 591	1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  adantlll  730  adantllr  731  adantl3r  762  isocnv  7330  f1iun  7942  odi  8565  oeoelem  8585  mapxpen  9132  xadddilem  13321  hashgt23el  14463  pcqmul  16914  infpnlem1  16971  setsn0fun  17234  chpdmat  22979  neitr  23318  hausflimi  24118  nmoix  24867  nmoleub  24869  metdsre  24992  bncssbn  25514  usgr2edg  29541  usgr2edg1  29543  crctcshwlkn0  30151  unoplin  32253  hmoplin  32275  chirredlem1  32723  mdsymlem2  32737  foresf1o  32831  zarcls1  34240  ordtconnlem1  34295  signstfvn  34937  isbasisrelowllem1  37982  isbasisrelowllem2  37983  pibt2  38044  lindsadd  38245  lindsdom  38246  matunitlindflem1  38248  matunitlindflem2  38249  poimirlem25  38277  poimirlem29  38281  heicant  38287  cnambfre  38300  itg2addnclem  38303  ftc1anclem5  38329  ftc1anc  38333  rrnequiv  38467  isfldidl  38700  ispridlc  38702  supxrgelem  46036  supminfxr  46161  uhgrimisgrgric  48679  cycl3grtri  48695  gpg5nbgrvtx03star  48828  gpg5nbgr3star  48829  itcovalt2lem2  49439  reccot  50519  rectan  50520