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  7350  f1iun  7968  odi  8617  oeoelem  8636  mapxpen  9183  xadddilem  13336  hashgt23el  14463  pcqmul  16891  infpnlem1  16948  setsn0fun  17210  chpdmat  22847  neitr  23188  hausflimi  23988  nmoix  24750  nmoleub  24752  metdsre  24875  bncssbn  25408  usgr2edg  29227  usgr2edg1  29229  crctcshwlkn0  29841  unoplin  31939  hmoplin  31961  chirredlem1  32409  mdsymlem2  32423  foresf1o  32523  zarcls1  33868  ordtconnlem1  33923  signstfvn  34584  isbasisrelowllem1  37356  isbasisrelowllem2  37357  pibt2  37418  lindsadd  37620  lindsdom  37621  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem25  37652  poimirlem29  37656  heicant  37662  cnambfre  37675  itg2addnclem  37678  ftc1anclem5  37704  ftc1anc  37708  rrnequiv  37842  isfldidl  38075  ispridlc  38077  supxrgelem  45348  supminfxr  45475  uhgrimisgrgric  47899  cycl3grtri  47914  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  itcovalt2lem2  48597  reccot  49277  rectan  49278