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  7318  f1iun  7929  odi  8552  oeoelem  8572  mapxpen  9119  xadddilem  13311  hashgt23el  14451  pcqmul  16903  infpnlem1  16960  setsn0fun  17223  chpdmat  22959  neitr  23298  hausflimi  24098  nmoix  24847  nmoleub  24849  metdsre  24972  bncssbn  25494  usgr2edg  29469  usgr2edg1  29471  crctcshwlkn0  30079  unoplin  32181  hmoplin  32203  chirredlem1  32651  mdsymlem2  32665  foresf1o  32760  zarcls1  34176  ordtconnlem1  34231  signstfvn  34873  isbasisrelowllem1  37861  isbasisrelowllem2  37862  pibt2  37923  lindsadd  38124  lindsdom  38125  matunitlindflem1  38127  matunitlindflem2  38128  poimirlem25  38156  poimirlem29  38160  heicant  38166  cnambfre  38179  itg2addnclem  38182  ftc1anclem5  38208  ftc1anc  38212  rrnequiv  38346  isfldidl  38579  ispridlc  38581  supxrgelem  45911  supminfxr  46036  uhgrimisgrgric  48551  cycl3grtri  48567  gpg5nbgrvtx03star  48700  gpg5nbgr3star  48701  itcovalt2lem2  49307  reccot  50387  rectan  50388