Theorem syld3an3 1319

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 1024	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1025	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1274	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  syld3an1  1320  syld3an2  1321  brelrng  4969  moriotass  6012  nnncan1  8457  lediv1  9091  modqval  10632  modqvalr  10633  modqcl  10634  flqpmodeq  10635  modq0  10637  modqge0  10640  modqlt  10641  modqdiffl  10643  modqdifz  10644  modqvalp1  10651  exp3val  10849  bcval4  11060  ccatval3  11225  ccatfv0  11229  ccatval1lsw  11230  ccatval21sw  11231  lswccatn0lsw  11237  pfxsuff1eqwrdeq  11329  pfxccatid  11371  dvdsmultr1  12455  dvdssub2  12459  divalglemeuneg  12547  ndvdsadd  12555  grpsubf  13725  grpinvsub  13728  grpnpcan  13738  mulginvcom  13797  mulginvinv  13798  subgsubcl  13835  qussub  13887  ghmsub  13901  dvrcl  14213  unitdvcl  14214  basgen2  14875  opnneiss  14952  cnpf2  15001  sincosq1lem  15619