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 618	. 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
3		sylanl1.2	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
4	2, 3	sylan 584	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  718  adantllr  719  adantl3r  750  isocnv  7075  f1iun  7647  odi  8213  oeoelem  8232  mapxpen  8702  xadddilem  12718  hashgt23el  13825  pcqmul  16235  infpnlem1  16291  setsn0fun  16568  chpdmat  21531  neitr  21870  hausflimi  22670  nmoix  23421  nmoleub  23423  metdsre  23544  bncssbn  24064  usgr2edg  27089  usgr2edg1  27091  crctcshwlkn0  27696  unoplin  29792  hmoplin  29814  chirredlem1  30262  mdsymlem2  30276  foresf1o  30362  zarcls1  31330  ordtconnlem1  31385  signstfvn  32057  isbasisrelowllem1  35042  isbasisrelowllem2  35043  pibt2  35104  lindsadd  35320  lindsdom  35321  matunitlindflem1  35323  matunitlindflem2  35324  poimirlem25  35352  poimirlem29  35356  heicant  35362  cnambfre  35375  itg2addnclem  35378  ftc1anclem5  35404  ftc1anc  35408  rrnequiv  35543  isfldidl  35776  ispridlc  35778  supxrgelem  42327  supminfxr  42459  itcovalt2lem2  45445  reccot  45639  rectan  45640