Theorem syld3an2 1535

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

Syntax hints:   → wi 4   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  nppcan2  10640  nnncan  10644  nnncan2  10646  subdivcomb2  11054  ltdivmul  11235  ledivmul  11236  ltdiv23  11251  lediv23  11252  xrmaxlt  12307  xrltmin  12308  xrmaxle  12309  xrlemin  12310  swrdtrcfvOLD  13737  pfxtrcfv  13779  pfxco  13966  dvdssub2  15407  dvdsgcdb  15642  lcmdvdsb  15706  vdwapun  16056  poslubdg  17509  ipodrsfi  17523  mulginvcom  17925  matinvgcell  20615  mdetrsca2  20785  mdetrlin2  20788  mdetunilem5  20797  decpmatmul  20954  islp3  21328  bddibl  24012  nvpi  28073  nvabs  28078  nmmulg  30553  lineid  32724  oplecon1b  35271  opltcon1b  35275  oldmm2  35288  oldmj2  35292  cmt3N  35321  2llnneN  35479  cvrexchlem  35489  pmod2iN  35919  polcon2N  35989  paddatclN  36019  osumcllem3N  36028  ltrnval1  36204  cdleme48fv  36569  cdlemg33b  36777  trlcolem  36796  cdlemh  36887  cdlemi1  36888  cdlemi2  36889  cdlemi  36890  cdlemk4  36904  cdlemk19u1  37039  cdlemn3  37267  hgmapfval  37956  pell14qrgap  38278  stoweidlem22  41027  stoweidlem26  41031  sigarexp  41836  lindszr  43119