Theorem syl3an1 1306

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  syl3an1b  1309  syl3an1br  1312  wepo  4456  f1ofveu  6005  fovcdmda  6165  smoiso  6467  tfrcl  6529  omv  6622  oeiv  6623  nndi  6653  nnmsucr  6655  f1oen2g  6927  f1dom2g  6928  undiffi  7116  prarloclemarch2  7638  distrnq0  7678  ltprordil  7808  1idprl  7809  1idpru  7810  ltpopr  7814  ltexprlemopu  7822  ltexprlemdisj  7825  ltexprlemfl  7828  ltexprlemfu  7830  ltexprlemru  7831  recexprlemdisj  7849  recexprlemss1l  7854  recexprlemss1u  7855  cnegexlem1  8353  msqge0  8795  mulge0  8798  divnegap  8885  divdiv32ap  8899  divneg2ap  8915  peano2uz  9816  lbzbi  9849  negqmod0  10592  modqmuladdnn0  10629  expnlbnd  10925  fun2dmnop  11111  shftfvalg  11378  xrmaxaddlem  11820  retanclap  12282  tannegap  12288  demoivreALT  12334  gcd0id  12549  isprm3  12689  euclemma  12717  phiprmpw  12793  fermltl  12805  sgrpcl  13491  mndcl  13505  imasmnd2  13534  grpcl  13590  dfgrp2  13609  grprcan  13619  grpsubcl  13662  imasgrp2  13696  mhmid  13701  mhmmnd  13702  mulginvcom  13733  mulgnndir  13737  mulgnnass  13743  qusgrp  13818  ghmmulg  13842  ghmrn  13843  ghmeqker  13857  ablcom  13889  ablinvadd  13896  ghmcmn  13913  rngacl  13954  rngpropd  13967  srgacl  13994  srgcom  13995  ringacl  14042  imasring  14076  subrngacl  14221  subrgacl  14245  subrgugrp  14253  lmodacl  14312  lmodmcl  14313  lmodvacl  14315  lmodvsubcl  14345  lmod4  14350  lmodvaddsub4  14352  lmodvpncan  14353  lmodvnpcan  14354  lmodsubeq0  14359  psmetcl  15049  xmetcl  15075  metcl  15076  meteq0  15083  metge0  15089  metsym  15094  blelrnps  15142  blelrn  15143  blssm  15144  blres  15157  mscl  15188  xmscl  15189  xmsge0  15190  xmseq0  15191  xmssym  15192  mopnin  15210  sincosq1sgn  15549  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  lgsneg1  15753  usgredg2vtx  16067  uspgredg2vtxeu  16068  usgredg2vtxeu  16069