Theorem syld3an2 1409

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 1134	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜑)
2		syld3an2.1	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
3		simp3 1136	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜃)
4		syld3an2.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1369	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  enfii  9191  domsdomtrfi  9207  nppcan2  11495  nnncan  11499  nnncan2  11501  subdivcomb2  11914  ltdivmul  12093  ledivmul  12094  ltdiv23  12109  lediv23  12110  xrmaxlt  13164  xrltmin  13165  xrmaxle  13166  xrlemin  13167  pfxtrcfv  14647  pfxco  14793  dvdssub2  16248  dvdsgcdb  16491  lcmdvdsb  16554  vdwapun  16911  poslubdg  18371  ipodrsfi  18496  mulginvcom  19015  matinvgcell  22157  mdetrsca2  22326  mdetrlin2  22329  mdetunilem5  22338  decpmatmul  22494  islp3  22870  bddibl  25589  nvpi  30187  nvabs  30192  nmmulg  33246  lineid  35359  oplecon1b  38374  opltcon1b  38378  oldmm2  38391  oldmj2  38395  cmt3N  38424  2llnneN  38583  cvrexchlem  38593  pmod2iN  39023  polcon2N  39093  paddatclN  39123  osumcllem3N  39132  ltrnval1  39308  cdleme48fv  39673  cdlemg33b  39881  trlcolem  39900  cdlemh  39991  cdlemi1  39992  cdlemi2  39993  cdlemi  39994  cdlemk4  40008  cdlemk19u1  40143  cdlemn3  40371  hgmapfval  41060  pell14qrgap  41915  mnringmulrcld  43289  stoweidlem22  45036  stoweidlem26  45040  sigarexp  45873  lindszr  47237  fv2arycl  47421