Theorem syld3an3 1427

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  brelrng  5913  resin  6824  moriotass  7380  omwordri  8535  oewordri  8556  dif1en  9124  sdomdomtrfi  9163  php3  9171  onomeneq  9176  preleqg  9564  gchaleph2  10624  gruf  10763  nnncan1  11461  lediv1  12051  lemuldiv  12066  ind1  12198  suprfinzcl  12681  supxrbnd  13325  bcval4  14314  ccatval3  14586  ccatfv0  14591  ccatval1lsw  14592  ccatval21sw  14593  lswccatn0lsw  14599  pfxsuff1eqwrdeq  14706  pfxccatid  14748  cshwidxmodr  14811  2swrd2eqwrdeq  14960  dvdsmultr1  16321  dvdssub2  16326  ndvdsadd  16435  mrcsscl  17643  latnle  18496  latabs1  18498  latabs2  18499  latj4rot  18513  grpsubf  19052  grpinvsub  19055  grpnpcan  19065  mulginvcom  19132  mulginvinv  19133  subgsubcl  19170  qussub  19223  ghmsub  19255  odhash3  19607  ogrpsublt  20173  srgcom4  20251  dvrcl  20440  unitdvcl  20441  abvsubtri  20864  lspsntrim  21153  frlmsslss2  21815  lindsmm  21868  ascldimul  21928  lply1binomsc  22362  smadiadetglem2  22720  m2cpm  22789  m2cpminvid  22801  pmatcollpwscmat  22839  mp2pm2mp  22859  cpmidgsum  22916  cpmadugsumfi  22925  basgen2  23037  opnneiss  23166  restlp  23231  nmtri  24674  csschl  25426  sincosq1lem  26550  logrec  26816  nosupbnd1lem2  27761  noinfbnd1lem2  27776  noetalem1  27793  grpodivinv  30696  grpoinvdiv  30697  grpodivf  30698  nvmval2  30803  nvaddsub4  30817  nvpi  30827  nvmtri  30831  nvabs  30832  4ipval2  30868  ipval3  30869  isblo2  30943  blof  30945  nmblore  30946  nmlnoubi  30956  nmlnogt0  30957  shsubcl  31380  unopadj  32079  atexch  32541  atcvatlem  32545  inelsiga  34393  inelros  34431  fineqvnttrclselem3  35380  revpfxsfxrev  35427  mrsubcv  35821  mrsubvr  35822  btwnconn2  36413  ismtybnd  38267  lkrlsp2  39688  opcon2b  39782  opltcon2b  39791  oldmm3N  39804  oldmm4  39805  oldmj3  39808  oldmj4  39809  cmt2N  39835  cmt4N  39837  atleneN  40019  lplnri2N  40139  cdlema2N  40377  pmapojoinN  40553  ltrncnvatb  40723  trlval2  40748  trljat1  40751  cdleme18c  40878  cdleme19c  40890  cdlemeiota  41170  trlcocnv  41305  tendoplco2  41364  cdlemk6  41422  cdlemk7u  41455  cdlemk22  41478  cdlemk24-3  41488  cdlemkid2  41509  cdlemk11ta  41514  cdlemk11tc  41530  cdlemk47  41534  cdlemk52  41539  tendocnv  41606  dibelval1st1  41735  dibelval1st2N  41736  dihord2pre2  41811  mzprename  43291  pell14qrdivcl  43403  pwssplit4  43627  iocmbl  43751  relexpxpmin  44254  dvconstbi  44871  limsupgtlem  46312  dvbdfbdioolem1  46463  ibliccsinexp  46486  stoweidlem22  46557  fourierdlem42  46684  smfsuplem1  47346  divsub1dir  49100