Theorem syld3an3 1316

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  syld3an1  1317  syld3an2  1318  brelrng  4954  moriotass  5984  nnncan1  8378  lediv1  9012  modqval  10541  modqvalr  10542  modqcl  10543  flqpmodeq  10544  modq0  10546  modqge0  10549  modqlt  10550  modqdiffl  10552  modqdifz  10553  modqvalp1  10560  exp3val  10758  bcval4  10969  ccatval3  11129  ccatfv0  11133  ccatval1lsw  11134  ccatval21sw  11135  lswccatn0lsw  11141  pfxsuff1eqwrdeq  11226  pfxccatid  11268  dvdsmultr1  12337  dvdssub2  12341  divalglemeuneg  12429  ndvdsadd  12437  grpsubf  13607  grpinvsub  13610  grpnpcan  13620  mulginvcom  13679  mulginvinv  13680  subgsubcl  13717  qussub  13769  ghmsub  13783  dvrcl  14093  unitdvcl  14094  basgen2  14749  opnneiss  14826  cnpf2  14875  sincosq1lem  15493