Theorem syld3an3 1417

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  brelrng  5883  resin  6789  moriotass  7345  omwordri  8497  oewordri  8518  dif1en  9086  sdomdomtrfi  9125  php3  9133  onomeneq  9138  preleqg  9527  gchaleph2  10586  gruf  10725  nnncan1  11421  lediv1  12012  lemuldiv  12027  ind1  12159  suprfinzcl  12634  supxrbnd  13271  bcval4  14260  ccatval3  14532  ccatfv0  14537  ccatval1lsw  14538  ccatval21sw  14539  lswccatn0lsw  14545  pfxsuff1eqwrdeq  14652  pfxccatid  14694  cshwidxmodr  14757  2swrd2eqwrdeq  14906  dvdsmultr1  16256  dvdssub2  16261  ndvdsadd  16370  mrcsscl  17577  latnle  18430  latabs1  18432  latabs2  18433  latj4rot  18447  grpsubf  18986  grpinvsub  18989  grpnpcan  18999  mulginvcom  19066  mulginvinv  19067  subgsubcl  19104  qussub  19157  ghmsub  19190  odhash3  19542  ogrpsublt  20108  srgcom4  20186  dvrcl  20375  unitdvcl  20376  abvsubtri  20799  lspsntrim  21088  frlmsslss2  21750  lindsmm  21803  ascldimul  21863  lply1binomsc  22297  smadiadetglem2  22655  m2cpm  22724  m2cpminvid  22736  pmatcollpwscmat  22774  mp2pm2mp  22794  cpmidgsum  22851  cpmadugsumfi  22860  basgen2  22972  opnneiss  23101  restlp  23166  nmtri  24609  csschl  25361  sincosq1lem  26479  logrec  26745  nosupbnd1lem2  27691  noinfbnd1lem2  27706  noetalem1  27723  grpodivinv  30625  grpoinvdiv  30626  grpodivf  30627  nvmval2  30732  nvaddsub4  30746  nvpi  30756  nvmtri  30760  nvabs  30761  4ipval2  30797  ipval3  30798  isblo2  30872  blof  30874  nmblore  30875  nmlnoubi  30885  nmlnogt0  30886  shsubcl  31309  unopadj  32008  atexch  32470  atcvatlem  32474  inelsiga  34319  inelros  34357  fineqvnttrclselem3  35304  revpfxsfxrev  35344  mrsubcv  35738  mrsubvr  35739  btwnconn2  36330  ismtybnd  38174  lkrlsp2  39595  opcon2b  39689  opltcon2b  39698  oldmm3N  39711  oldmm4  39712  oldmj3  39715  oldmj4  39716  cmt2N  39742  cmt4N  39744  atleneN  39926  lplnri2N  40046  cdlema2N  40284  pmapojoinN  40460  ltrncnvatb  40630  trlval2  40655  trljat1  40658  cdleme18c  40785  cdleme19c  40797  cdlemeiota  41077  trlcocnv  41212  tendoplco2  41271  cdlemk6  41329  cdlemk7u  41362  cdlemk22  41385  cdlemk24-3  41395  cdlemkid2  41416  cdlemk11ta  41421  cdlemk11tc  41437  cdlemk47  41441  cdlemk52  41446  tendocnv  41513  dibelval1st1  41642  dibelval1st2N  41643  dihord2pre2  41718  mzprename  43198  pell14qrdivcl  43310  pwssplit4  43534  iocmbl  43658  relexpxpmin  44161  dvconstbi  44778  limsupgtlem  46220  dvbdfbdioolem1  46371  ibliccsinexp  46394  stoweidlem22  46465  fourierdlem42  46592  smfsuplem1  47254  divsub1dir  49008