Theorem syld3an3 1409

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 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1371	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  brelrng  5966  resin  6884  moriotass  7437  omwordri  8628  oewordri  8648  dif1en  9226  dif1enOLD  9228  sdomdomtrfi  9267  php3  9275  onomeneq  9291  preleqg  9684  gchaleph2  10741  gruf  10880  nnncan1  11572  lediv1  12160  lemuldiv  12175  suprfinzcl  12757  supxrbnd  13390  bcval4  14356  ccatval3  14627  ccatfv0  14631  ccatval1lsw  14632  ccatval21sw  14633  lswccatn0lsw  14639  pfxsuff1eqwrdeq  14747  pfxccatid  14789  cshwidxmodr  14852  2swrd2eqwrdeq  15002  dvdsmultr1  16344  dvdssub2  16349  ndvdsadd  16458  mrcsscl  17678  latnle  18543  latabs1  18545  latabs2  18546  latj4rot  18560  grpsubf  19059  grpinvsub  19062  grpnpcan  19072  mulginvcom  19139  mulginvinv  19140  subgsubcl  19177  qussub  19231  ghmsub  19264  odhash3  19618  srgcom4  20241  dvrcl  20430  unitdvcl  20431  abvsubtri  20850  lspsntrim  21120  frlmsslss2  21818  lindsmm  21871  ascldimul  21931  lply1binomsc  22336  smadiadetglem2  22699  m2cpm  22768  m2cpminvid  22780  pmatcollpwscmat  22818  mp2pm2mp  22838  cpmidgsum  22895  cpmadugsumfi  22904  basgen2  23017  opnneiss  23147  restlp  23212  nmtri  24660  csschl  25429  sincosq1lem  26557  logrec  26824  nosupbnd1lem2  27772  noinfbnd1lem2  27787  noetalem1  27804  grpodivinv  30568  grpoinvdiv  30569  grpodivf  30570  nvmval2  30675  nvaddsub4  30689  nvpi  30699  nvmtri  30703  nvabs  30704  4ipval2  30740  ipval3  30741  isblo2  30815  blof  30817  nmblore  30818  nmlnoubi  30828  nmlnogt0  30829  shsubcl  31252  unopadj  31951  atexch  32413  atcvatlem  32417  ogrpsublt  33071  ind1  33981  inelsiga  34099  inelros  34137  revpfxsfxrev  35083  mrsubcv  35478  mrsubvr  35479  btwnconn2  36066  ismtybnd  37767  lkrlsp2  39059  opcon2b  39153  opltcon2b  39162  oldmm3N  39175  oldmm4  39176  oldmj3  39179  oldmj4  39180  cmt2N  39206  cmt4N  39208  atleneN  39391  lplnri2N  39511  cdlema2N  39749  pmapojoinN  39925  ltrncnvatb  40095  trlval2  40120  trljat1  40123  cdleme18c  40250  cdleme19c  40262  cdlemeiota  40542  trlcocnv  40677  tendoplco2  40736  cdlemk6  40794  cdlemk7u  40827  cdlemk22  40850  cdlemk24-3  40860  cdlemkid2  40881  cdlemk11ta  40886  cdlemk11tc  40902  cdlemk47  40906  cdlemk52  40911  tendocnv  40978  dibelval1st1  41107  dibelval1st2N  41108  dihord2pre2  41183  mzprename  42705  pell14qrdivcl  42821  pwssplit4  43046  iocmbl  43174  relexpxpmin  43679  dvconstbi  44303  limsupgtlem  45698  dvbdfbdioolem1  45849  ibliccsinexp  45872  stoweidlem22  45943  fourierdlem42  46070  smfsuplem1  46732  divsub1dir  48246