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 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  syld3an1  1324  syld3an2  1325  brelrng  5008  moriotass  6059  nnncan1  8552  lediv1  9189  modqval  10739  modqvalr  10740  modqcl  10741  flqpmodeq  10742  modq0  10744  modqge0  10747  modqlt  10748  modqdiffl  10750  modqdifz  10751  modqvalp1  10758  exp3val  10956  bcval4  11168  ccatval3  11345  ccatfv0  11349  ccatval1lsw  11350  ccatval21sw  11351  lswccatn0lsw  11357  pfxsuff1eqwrdeq  11449  pfxccatid  11491  dvdsmultr1  12576  dvdssub2  12580  divalglemeuneg  12668  ndvdsadd  12676  grpsubf  13861  grpinvsub  13864  grpnpcan  13874  mulginvcom  13927  mulginvinv  13928  subgsubcl  13965  qussub  14017  ghmsub  14031  dvrcl  14415  unitdvcl  14416  basgen2  15105  opnneiss  15182  cnpf2  15231  sincosq1lem  15849