Theorem syld3an3 1405

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

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

Assertion

Ref	Expression
syld3an3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 1132	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1133	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1367	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  brelrng  5811  resin  6636  moriotass  7146  omwordri  8198  oewordri  8218  preleqg  9078  gchaleph2  10094  gruf  10233  nnncan1  10922  lediv1  11505  lemuldiv  11520  suprfinzcl  12098  supxrbnd  12722  bcval4  13668  ccatval3  13933  ccatfv0  13937  ccatval1lsw  13938  ccatval21sw  13939  lswccatn0lsw  13945  pfxsuff1eqwrdeq  14061  pfxccatid  14103  cshwidxmodr  14166  2swrd2eqwrdeq  14315  dvdsmultr1  15647  dvdssub2  15651  ndvdsadd  15761  mrcsscl  16891  latnle  17695  latabs1  17697  latabs2  17698  latj4rot  17712  grpsubf  18178  grpinvsub  18181  grpnpcan  18191  mulginvcom  18252  mulginvinv  18253  subgsubcl  18290  qussub  18340  ghmsub  18366  odhash3  18701  dvrcl  19436  unitdvcl  19437  abvsubtri  19606  lspsntrim  19870  ascldimul  20116  lply1binomsc  20475  frlmsslss2  20919  lindsmm  20972  smadiadetglem2  21281  m2cpm  21349  m2cpminvid  21361  pmatcollpwscmat  21399  mp2pm2mp  21419  cpmidgsum  21476  cpmadugsumfi  21485  basgen2  21597  opnneiss  21726  restlp  21791  nmtri  23235  csschl  23979  sincosq1lem  25083  logrec  25341  grpodivinv  28313  grpoinvdiv  28314  grpodivf  28315  nvmval2  28420  nvaddsub4  28434  nvpi  28444  nvmtri  28448  nvabs  28449  4ipval2  28485  ipval3  28486  isblo2  28560  blof  28562  nmblore  28563  nmlnoubi  28573  nmlnogt0  28574  shsubcl  28997  unopadj  29696  atexch  30158  atcvatlem  30162  ogrpsublt  30722  ind1  31276  inelsiga  31394  inelros  31432  revpfxsfxrev  32362  mrsubcv  32757  mrsubvr  32758  nosupbnd1lem2  33209  btwnconn2  33563  ismtybnd  35100  lkrlsp2  36254  opcon2b  36348  opltcon2b  36357  oldmm3N  36370  oldmm4  36371  oldmj3  36374  oldmj4  36375  cmt2N  36401  cmt4N  36403  atleneN  36585  lplnri2N  36705  cdlema2N  36943  pmapojoinN  37119  ltrncnvatb  37289  trlval2  37314  trljat1  37317  cdleme18c  37444  cdleme19c  37456  cdlemeiota  37736  trlcocnv  37871  tendoplco2  37930  cdlemk6  37988  cdlemk7u  38021  cdlemk22  38044  cdlemk24-3  38054  cdlemkid2  38075  cdlemk11ta  38080  cdlemk11tc  38096  cdlemk47  38100  cdlemk52  38105  tendocnv  38172  dibelval1st1  38301  dibelval1st2N  38302  dihord2pre2  38377  mzprename  39395  pell14qrdivcl  39511  pwssplit4  39738  iocmbl  39868  relexpxpmin  40111  dvconstbi  40715  limsupgtlem  42107  dvbdfbdioolem1  42262  ibliccsinexp  42285  stoweidlem22  42356  fourierdlem42  42483  smfsuplem1  43134  divsub1dir  44621