Theorem syl3an1 1282

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 1187	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
3		syl3an1.2	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
4	2, 3	syl 14	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  syl3an1b  1285  syl3an1br  1288  wepo  4395  f1ofveu  5913  fovcdmda  6071  smoiso  6369  tfrcl  6431  omv  6522  oeiv  6523  nndi  6553  nnmsucr  6555  f1oen2g  6823  f1dom2g  6824  undiffi  6995  prarloclemarch2  7505  distrnq0  7545  ltprordil  7675  1idprl  7676  1idpru  7677  ltpopr  7681  ltexprlemopu  7689  ltexprlemdisj  7692  ltexprlemfl  7695  ltexprlemfu  7697  ltexprlemru  7698  recexprlemdisj  7716  recexprlemss1l  7721  recexprlemss1u  7722  cnegexlem1  8220  msqge0  8662  mulge0  8665  divnegap  8752  divdiv32ap  8766  divneg2ap  8782  peano2uz  9676  lbzbi  9709  negqmod0  10442  modqmuladdnn0  10479  expnlbnd  10775  shftfvalg  11002  xrmaxaddlem  11444  retanclap  11906  tannegap  11912  demoivreALT  11958  gcd0id  12173  isprm3  12313  euclemma  12341  phiprmpw  12417  fermltl  12429  sgrpcl  13113  mndcl  13127  imasmnd2  13156  grpcl  13212  dfgrp2  13231  grprcan  13241  grpsubcl  13284  imasgrp2  13318  mhmid  13323  mhmmnd  13324  mulginvcom  13355  mulgnndir  13359  mulgnnass  13365  qusgrp  13440  ghmmulg  13464  ghmrn  13465  ghmeqker  13479  ablcom  13511  ablinvadd  13518  ghmcmn  13535  rngacl  13576  rngpropd  13589  srgacl  13616  srgcom  13617  ringacl  13664  imasring  13698  subrngacl  13842  subrgacl  13866  subrgugrp  13874  lmodacl  13933  lmodmcl  13934  lmodvacl  13936  lmodvsubcl  13966  lmod4  13971  lmodvaddsub4  13973  lmodvpncan  13974  lmodvnpcan  13975  lmodsubeq0  13980  psmetcl  14670  xmetcl  14696  metcl  14697  meteq0  14704  metge0  14710  metsym  14715  blelrnps  14763  blelrn  14764  blssm  14765  blres  14778  mscl  14809  xmscl  14810  xmsge0  14811  xmseq0  14812  xmssym  14813  mopnin  14831  sincosq1sgn  15170  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  lgsneg1  15374