Theorem sylanl1 693

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  adantlll  731  adantllr  732  adantl3r  763  isocnv  7335  f1iun  7945  odi  8570  oeoelem  8590  mapxpen  9145  xadddilem  13350  hashgt23el  14493  pcqmul  16951  infpnlem1  17008  setsn0fun  17271  lindsdom  22069  matunitlindflem1  22907  matunitlindflem2  22908  chpdmat  23072  neitr  23411  hausflimi  24212  nmoix  24961  nmoleub  24963  metdsre  25086  bncssbn  25608  usgr2edg  29678  usgr2edg1  29680  crctcshwlkn0  30297  unoplin  32409  hmoplin  32431  chirredlem1  32879  mdsymlem2  32893  foresf1o  32987  zarcls1  34387  ordtconnlem1  34442  signstfvn  35085  isbasisrelowllem1  38117  isbasisrelowllem2  38118  pibt2  38179  lindsadd  38375  poimirlem25  38402  poimirlem29  38406  heicant  38412  cnambfre  38425  itg2addnclem  38428  ftc1anclem5  38454  ftc1anc  38458  rrnequiv  38593  isfldidl  38826  ispridlc  38828  supxrgelem  46175  supminfxr  46300  uhgrimisgrgric  48855  cycl3grtri  48871  gpg5nbgrvtx03star  49004  gpg5nbgr3star  49005  itcovalt2lem2  49614  reccot  50692  rectan  50693