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  7271  f1iun  7886  odi  8504  oeoelem  8523  mapxpen  9067  xadddilem  13214  hashgt23el  14349  pcqmul  16783  infpnlem1  16840  setsn0fun  17102  chpdmat  22744  neitr  23083  hausflimi  23883  nmoix  24633  nmoleub  24635  metdsre  24758  bncssbn  25290  usgr2edg  29173  usgr2edg1  29175  crctcshwlkn0  29784  unoplin  31882  hmoplin  31904  chirredlem1  32352  mdsymlem2  32366  foresf1o  32466  zarcls1  33835  ordtconnlem1  33890  signstfvn  34536  isbasisrelowllem1  37328  isbasisrelowllem2  37329  pibt2  37390  lindsadd  37592  lindsdom  37593  matunitlindflem1  37595  matunitlindflem2  37596  poimirlem25  37624  poimirlem29  37628  heicant  37634  cnambfre  37647  itg2addnclem  37650  ftc1anclem5  37676  ftc1anc  37680  rrnequiv  37814  isfldidl  38047  ispridlc  38049  supxrgelem  45317  supminfxr  45444  uhgrimisgrgric  47916  cycl3grtri  47932  gpg5nbgrvtx03star  48065  gpg5nbgr3star  48066  itcovalt2lem2  48662  reccot  49744  rectan  49745