Theorem syld3an3 1412

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 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1138	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1374	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  5898  resin  6804  moriotass  7357  omwordri  8509  oewordri  8530  dif1en  9098  sdomdomtrfi  9137  php3  9145  onomeneq  9150  preleqg  9536  gchaleph2  10595  gruf  10734  nnncan1  11429  lediv1  12019  lemuldiv  12034  suprfinzcl  12618  supxrbnd  13255  bcval4  14242  ccatval3  14514  ccatfv0  14519  ccatval1lsw  14520  ccatval21sw  14521  lswccatn0lsw  14527  pfxsuff1eqwrdeq  14634  pfxccatid  14676  cshwidxmodr  14739  2swrd2eqwrdeq  14888  dvdsmultr1  16235  dvdssub2  16240  ndvdsadd  16349  mrcsscl  17555  latnle  18408  latabs1  18410  latabs2  18411  latj4rot  18425  grpsubf  18961  grpinvsub  18964  grpnpcan  18974  mulginvcom  19041  mulginvinv  19042  subgsubcl  19079  qussub  19132  ghmsub  19165  odhash3  19517  ogrpsublt  20083  srgcom4  20161  dvrcl  20352  unitdvcl  20353  abvsubtri  20772  lspsntrim  21062  frlmsslss2  21742  lindsmm  21795  ascldimul  21856  lply1binomsc  22267  smadiadetglem2  22628  m2cpm  22697  m2cpminvid  22709  pmatcollpwscmat  22747  mp2pm2mp  22767  cpmidgsum  22824  cpmadugsumfi  22833  basgen2  22945  opnneiss  23074  restlp  23139  nmtri  24582  csschl  25344  sincosq1lem  26474  logrec  26741  nosupbnd1lem2  27689  noinfbnd1lem2  27704  noetalem1  27721  grpodivinv  30624  grpoinvdiv  30625  grpodivf  30626  nvmval2  30731  nvaddsub4  30745  nvpi  30755  nvmtri  30759  nvabs  30760  4ipval2  30796  ipval3  30797  isblo2  30871  blof  30873  nmblore  30874  nmlnoubi  30884  nmlnogt0  30885  shsubcl  31308  unopadj  32007  atexch  32469  atcvatlem  32473  ind1  32947  inelsiga  34313  inelros  34351  fineqvnttrclselem3  35301  revpfxsfxrev  35332  mrsubcv  35726  mrsubvr  35727  btwnconn2  36318  ismtybnd  38058  lkrlsp2  39479  opcon2b  39573  opltcon2b  39582  oldmm3N  39595  oldmm4  39596  oldmj3  39599  oldmj4  39600  cmt2N  39626  cmt4N  39628  atleneN  39810  lplnri2N  39930  cdlema2N  40168  pmapojoinN  40344  ltrncnvatb  40514  trlval2  40539  trljat1  40542  cdleme18c  40669  cdleme19c  40681  cdlemeiota  40961  trlcocnv  41096  tendoplco2  41155  cdlemk6  41213  cdlemk7u  41246  cdlemk22  41269  cdlemk24-3  41279  cdlemkid2  41300  cdlemk11ta  41305  cdlemk11tc  41321  cdlemk47  41325  cdlemk52  41330  tendocnv  41397  dibelval1st1  41526  dibelval1st2N  41527  dihord2pre2  41602  mzprename  43106  pell14qrdivcl  43222  pwssplit4  43446  iocmbl  43570  relexpxpmin  44073  dvconstbi  44690  limsupgtlem  46135  dvbdfbdioolem1  46286  ibliccsinexp  46309  stoweidlem22  46380  fourierdlem42  46507  smfsuplem1  47169  divsub1dir  48877