Theorem syld3an3 1410

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 1372	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  brelrng  5932  resin  6850  moriotass  7402  omwordri  8592  oewordri  8612  dif1en  9182  dif1enOLD  9184  sdomdomtrfi  9223  php3  9231  onomeneq  9247  preleqg  9637  gchaleph2  10694  gruf  10833  nnncan1  11527  lediv1  12115  lemuldiv  12130  suprfinzcl  12715  supxrbnd  13352  bcval4  14329  ccatval3  14600  ccatfv0  14604  ccatval1lsw  14605  ccatval21sw  14606  lswccatn0lsw  14612  pfxsuff1eqwrdeq  14720  pfxccatid  14762  cshwidxmodr  14825  2swrd2eqwrdeq  14975  dvdsmultr1  16316  dvdssub2  16321  ndvdsadd  16430  mrcsscl  17635  latnle  18488  latabs1  18490  latabs2  18491  latj4rot  18505  grpsubf  19007  grpinvsub  19010  grpnpcan  19020  mulginvcom  19087  mulginvinv  19088  subgsubcl  19125  qussub  19179  ghmsub  19212  odhash3  19563  srgcom4  20180  dvrcl  20373  unitdvcl  20374  abvsubtri  20797  lspsntrim  21066  frlmsslss2  21750  lindsmm  21803  ascldimul  21863  lply1binomsc  22264  smadiadetglem2  22627  m2cpm  22696  m2cpminvid  22708  pmatcollpwscmat  22746  mp2pm2mp  22766  cpmidgsum  22823  cpmadugsumfi  22832  basgen2  22944  opnneiss  23073  restlp  23138  nmtri  24584  csschl  25347  sincosq1lem  26476  logrec  26743  nosupbnd1lem2  27691  noinfbnd1lem2  27706  noetalem1  27723  grpodivinv  30484  grpoinvdiv  30485  grpodivf  30486  nvmval2  30591  nvaddsub4  30605  nvpi  30615  nvmtri  30619  nvabs  30620  4ipval2  30656  ipval3  30657  isblo2  30731  blof  30733  nmblore  30734  nmlnoubi  30744  nmlnogt0  30745  shsubcl  31168  unopadj  31867  atexch  32329  atcvatlem  32333  ind1  32787  ogrpsublt  33042  inelsiga  34111  inelros  34149  revpfxsfxrev  35096  mrsubcv  35490  mrsubvr  35491  btwnconn2  36078  ismtybnd  37789  lkrlsp2  39079  opcon2b  39173  opltcon2b  39182  oldmm3N  39195  oldmm4  39196  oldmj3  39199  oldmj4  39200  cmt2N  39226  cmt4N  39228  atleneN  39411  lplnri2N  39531  cdlema2N  39769  pmapojoinN  39945  ltrncnvatb  40115  trlval2  40140  trljat1  40143  cdleme18c  40270  cdleme19c  40282  cdlemeiota  40562  trlcocnv  40697  tendoplco2  40756  cdlemk6  40814  cdlemk7u  40847  cdlemk22  40870  cdlemk24-3  40880  cdlemkid2  40901  cdlemk11ta  40906  cdlemk11tc  40922  cdlemk47  40926  cdlemk52  40931  tendocnv  40998  dibelval1st1  41127  dibelval1st2N  41128  dihord2pre2  41203  mzprename  42738  pell14qrdivcl  42854  pwssplit4  43079  iocmbl  43203  relexpxpmin  43707  dvconstbi  44325  limsupgtlem  45764  dvbdfbdioolem1  45915  ibliccsinexp  45938  stoweidlem22  46009  fourierdlem42  46136  smfsuplem1  46798  divsub1dir  48407