Theorem syl3an1 1283

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)

Hypotheses

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

Assertion

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

Proof of Theorem syl3an1

Step	Hyp	Ref	Expression
1		syl3an1.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	3anim1i 1188	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 14	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  syl3an1b  1286  syl3an1br  1289  wepo  4414  f1ofveu  5945  fovcdmda  6103  smoiso  6401  tfrcl  6463  omv  6554  oeiv  6555  nndi  6585  nnmsucr  6587  f1oen2g  6859  f1dom2g  6860  undiffi  7037  prarloclemarch2  7552  distrnq0  7592  ltprordil  7722  1idprl  7723  1idpru  7724  ltpopr  7728  ltexprlemopu  7736  ltexprlemdisj  7739  ltexprlemfl  7742  ltexprlemfu  7744  ltexprlemru  7745  recexprlemdisj  7763  recexprlemss1l  7768  recexprlemss1u  7769  cnegexlem1  8267  msqge0  8709  mulge0  8712  divnegap  8799  divdiv32ap  8813  divneg2ap  8829  peano2uz  9724  lbzbi  9757  negqmod0  10498  modqmuladdnn0  10535  expnlbnd  10831  fun2dmnop  11015  shftfvalg  11204  xrmaxaddlem  11646  retanclap  12108  tannegap  12114  demoivreALT  12160  gcd0id  12375  isprm3  12515  euclemma  12543  phiprmpw  12619  fermltl  12631  sgrpcl  13316  mndcl  13330  imasmnd2  13359  grpcl  13415  dfgrp2  13434  grprcan  13444  grpsubcl  13487  imasgrp2  13521  mhmid  13526  mhmmnd  13527  mulginvcom  13558  mulgnndir  13562  mulgnnass  13568  qusgrp  13643  ghmmulg  13667  ghmrn  13668  ghmeqker  13682  ablcom  13714  ablinvadd  13721  ghmcmn  13738  rngacl  13779  rngpropd  13792  srgacl  13819  srgcom  13820  ringacl  13867  imasring  13901  subrngacl  14045  subrgacl  14069  subrgugrp  14077  lmodacl  14136  lmodmcl  14137  lmodvacl  14139  lmodvsubcl  14169  lmod4  14174  lmodvaddsub4  14176  lmodvpncan  14177  lmodvnpcan  14178  lmodsubeq0  14183  psmetcl  14873  xmetcl  14899  metcl  14900  meteq0  14907  metge0  14913  metsym  14918  blelrnps  14966  blelrn  14967  blssm  14968  blres  14981  mscl  15012  xmscl  15013  xmsge0  15014  xmseq0  15015  xmssym  15016  mopnin  15034  sincosq1sgn  15373  sincosq2sgn  15374  sincosq3sgn  15375  sincosq4sgn  15376  lgsneg1  15577