Theorem syld3an3 1323

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

Ref	Expression
syld3an3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
syld3an3.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syld3an3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 1028	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1029	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syld3an1  1324  syld3an2  1325  brelrng  5013  moriotass  6069  nnncan1  8563  lediv1  9201  ind1  9302  modqval  10774  modqvalr  10775  modqcl  10776  flqpmodeq  10777  modq0  10779  modqge0  10782  modqlt  10783  modqdiffl  10785  modqdifz  10786  modqvalp1  10793  exp3val  10991  bcval4  11204  ccatval3  11381  ccatfv0  11385  ccatval1lsw  11386  ccatval21sw  11387  lswccatn0lsw  11393  pfxsuff1eqwrdeq  11485  pfxccatid  11527  dvdsmultr1  12614  dvdssub2  12618  divalglemeuneg  12706  ndvdsadd  12714  grpsubf  13933  grpinvsub  13936  grpnpcan  13946  mulginvcom  13999  mulginvinv  14000  subgsubcl  14037  qussub  14089  ghmsub  14103  dvrcl  14491  unitdvcl  14492  ascldimul  15080  basgen2  15231  opnneiss  15308  cnpf2  15357  sincosq1lem  15976