Theorem syld3an2 1414

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

Hypotheses

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

Assertion

Ref	Expression
syld3an2	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Proof of Theorem syld3an2

Step	Hyp	Ref	Expression
1		simp1 1137	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑)
2		syld3an2.1	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3		simp3 1139	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃)
4		syld3an2.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1374	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  enfii  9120  domsdomtrfi  9136  nppcan2  11425  nnncan  11429  nnncan2  11431  div11  11837  subdivcomb2  11851  ltdivmul  12031  ledivmul  12032  ltdiv23  12047  lediv23  12048  xrmaxlt  13133  xrltmin  13134  xrmaxle  13135  xrlemin  13136  pfxtrcfv  14655  pfxco  14800  dvdssub2  16270  dvdsgcdb  16514  lcmdvdsb  16582  vdwapun  16945  poslubdg  18378  ipodrsfi  18505  mulginvcom  19075  matinvgcell  22400  mdetrsca2  22569  mdetrlin2  22572  mdetunilem5  22581  decpmatmul  22737  islp3  23111  bddibl  25807  nvpi  30738  nvabs  30743  nmmulg  34110  fineqvnttrclselem2  35266  fineqvnttrclselem3  35267  lineid  36265  oplecon1b  39647  opltcon1b  39651  oldmm2  39664  oldmj2  39668  cmt3N  39697  2llnneN  39855  cvrexchlem  39865  pmod2iN  40295  polcon2N  40365  paddatclN  40395  osumcllem3N  40404  ltrnval1  40580  cdleme48fv  40945  cdlemg33b  41153  trlcolem  41172  cdlemh  41263  cdlemi1  41264  cdlemi2  41265  cdlemi  41266  cdlemk4  41280  cdlemk19u1  41415  cdlemn3  41643  hgmapfval  42332  pell14qrgap  43303  mnringmulrcld  44655  stoweidlem22  46450  stoweidlem26  46454  sigarexp  47287  lindszr  48945  fv2arycl  49124