Theorem syld3an3 1411

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 1373	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  5908  resin  6825  moriotass  7379  omwordri  8539  oewordri  8559  dif1en  9130  dif1enOLD  9132  sdomdomtrfi  9171  php3  9179  onomeneq  9184  preleqg  9575  gchaleph2  10632  gruf  10771  nnncan1  11465  lediv1  12055  lemuldiv  12070  suprfinzcl  12655  supxrbnd  13295  bcval4  14279  ccatval3  14551  ccatfv0  14555  ccatval1lsw  14556  ccatval21sw  14557  lswccatn0lsw  14563  pfxsuff1eqwrdeq  14671  pfxccatid  14713  cshwidxmodr  14776  2swrd2eqwrdeq  14926  dvdsmultr1  16273  dvdssub2  16278  ndvdsadd  16387  mrcsscl  17588  latnle  18439  latabs1  18441  latabs2  18442  latj4rot  18456  grpsubf  18958  grpinvsub  18961  grpnpcan  18971  mulginvcom  19038  mulginvinv  19039  subgsubcl  19076  qussub  19130  ghmsub  19163  odhash3  19513  srgcom4  20130  dvrcl  20320  unitdvcl  20321  abvsubtri  20743  lspsntrim  21012  frlmsslss2  21691  lindsmm  21744  ascldimul  21804  lply1binomsc  22205  smadiadetglem2  22566  m2cpm  22635  m2cpminvid  22647  pmatcollpwscmat  22685  mp2pm2mp  22705  cpmidgsum  22762  cpmadugsumfi  22771  basgen2  22883  opnneiss  23012  restlp  23077  nmtri  24521  csschl  25283  sincosq1lem  26413  logrec  26680  nosupbnd1lem2  27628  noinfbnd1lem2  27643  noetalem1  27660  grpodivinv  30472  grpoinvdiv  30473  grpodivf  30474  nvmval2  30579  nvaddsub4  30593  nvpi  30603  nvmtri  30607  nvabs  30608  4ipval2  30644  ipval3  30645  isblo2  30719  blof  30721  nmblore  30722  nmlnoubi  30732  nmlnogt0  30733  shsubcl  31156  unopadj  31855  atexch  32317  atcvatlem  32321  ind1  32787  ogrpsublt  33042  inelsiga  34132  inelros  34170  revpfxsfxrev  35110  mrsubcv  35504  mrsubvr  35505  btwnconn2  36097  ismtybnd  37808  lkrlsp2  39103  opcon2b  39197  opltcon2b  39206  oldmm3N  39219  oldmm4  39220  oldmj3  39223  oldmj4  39224  cmt2N  39250  cmt4N  39252  atleneN  39435  lplnri2N  39555  cdlema2N  39793  pmapojoinN  39969  ltrncnvatb  40139  trlval2  40164  trljat1  40167  cdleme18c  40294  cdleme19c  40306  cdlemeiota  40586  trlcocnv  40721  tendoplco2  40780  cdlemk6  40838  cdlemk7u  40871  cdlemk22  40894  cdlemk24-3  40904  cdlemkid2  40925  cdlemk11ta  40930  cdlemk11tc  40946  cdlemk47  40950  cdlemk52  40955  tendocnv  41022  dibelval1st1  41151  dibelval1st2N  41152  dihord2pre2  41227  mzprename  42744  pell14qrdivcl  42860  pwssplit4  43085  iocmbl  43209  relexpxpmin  43713  dvconstbi  44330  limsupgtlem  45782  dvbdfbdioolem1  45933  ibliccsinexp  45956  stoweidlem22  46027  fourierdlem42  46154  smfsuplem1  46816  divsub1dir  48510