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  4404  f1ofveu  5922  fovcdmda  6080  smoiso  6378  tfrcl  6440  omv  6531  oeiv  6532  nndi  6562  nnmsucr  6564  f1oen2g  6832  f1dom2g  6833  undiffi  7004  prarloclemarch2  7514  distrnq0  7554  ltprordil  7684  1idprl  7685  1idpru  7686  ltpopr  7690  ltexprlemopu  7698  ltexprlemdisj  7701  ltexprlemfl  7704  ltexprlemfu  7706  ltexprlemru  7707  recexprlemdisj  7725  recexprlemss1l  7730  recexprlemss1u  7731  cnegexlem1  8229  msqge0  8671  mulge0  8674  divnegap  8761  divdiv32ap  8775  divneg2ap  8791  peano2uz  9686  lbzbi  9719  negqmod0  10457  modqmuladdnn0  10494  expnlbnd  10790  shftfvalg  11048  xrmaxaddlem  11490  retanclap  11952  tannegap  11958  demoivreALT  12004  gcd0id  12219  isprm3  12359  euclemma  12387  phiprmpw  12463  fermltl  12475  sgrpcl  13159  mndcl  13173  imasmnd2  13202  grpcl  13258  dfgrp2  13277  grprcan  13287  grpsubcl  13330  imasgrp2  13364  mhmid  13369  mhmmnd  13370  mulginvcom  13401  mulgnndir  13405  mulgnnass  13411  qusgrp  13486  ghmmulg  13510  ghmrn  13511  ghmeqker  13525  ablcom  13557  ablinvadd  13564  ghmcmn  13581  rngacl  13622  rngpropd  13635  srgacl  13662  srgcom  13663  ringacl  13710  imasring  13744  subrngacl  13888  subrgacl  13912  subrgugrp  13920  lmodacl  13979  lmodmcl  13980  lmodvacl  13982  lmodvsubcl  14012  lmod4  14017  lmodvaddsub4  14019  lmodvpncan  14020  lmodvnpcan  14021  lmodsubeq0  14026  psmetcl  14716  xmetcl  14742  metcl  14743  meteq0  14750  metge0  14756  metsym  14761  blelrnps  14809  blelrn  14810  blssm  14811  blres  14824  mscl  14855  xmscl  14856  xmsge0  14857  xmseq0  14858  xmssym  14859  mopnin  14877  sincosq1sgn  15216  sincosq2sgn  15217  sincosq3sgn  15218  sincosq4sgn  15219  lgsneg1  15420