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  5894  resin  6804  moriotass  7358  omwordri  8513  oewordri  8533  dif1en  9101  dif1enOLD  9103  sdomdomtrfi  9142  php3  9150  onomeneq  9155  preleqg  9544  gchaleph2  10601  gruf  10740  nnncan1  11434  lediv1  12024  lemuldiv  12039  suprfinzcl  12624  supxrbnd  13264  bcval4  14248  ccatval3  14520  ccatfv0  14524  ccatval1lsw  14525  ccatval21sw  14526  lswccatn0lsw  14532  pfxsuff1eqwrdeq  14640  pfxccatid  14682  cshwidxmodr  14745  2swrd2eqwrdeq  14895  dvdsmultr1  16242  dvdssub2  16247  ndvdsadd  16356  mrcsscl  17557  latnle  18408  latabs1  18410  latabs2  18411  latj4rot  18425  grpsubf  18927  grpinvsub  18930  grpnpcan  18940  mulginvcom  19007  mulginvinv  19008  subgsubcl  19045  qussub  19099  ghmsub  19132  odhash3  19482  srgcom4  20099  dvrcl  20289  unitdvcl  20290  abvsubtri  20712  lspsntrim  20981  frlmsslss2  21660  lindsmm  21713  ascldimul  21773  lply1binomsc  22174  smadiadetglem2  22535  m2cpm  22604  m2cpminvid  22616  pmatcollpwscmat  22654  mp2pm2mp  22674  cpmidgsum  22731  cpmadugsumfi  22740  basgen2  22852  opnneiss  22981  restlp  23046  nmtri  24490  csschl  25252  sincosq1lem  26382  logrec  26649  nosupbnd1lem2  27597  noinfbnd1lem2  27612  noetalem1  27629  grpodivinv  30438  grpoinvdiv  30439  grpodivf  30440  nvmval2  30545  nvaddsub4  30559  nvpi  30569  nvmtri  30573  nvabs  30574  4ipval2  30610  ipval3  30611  isblo2  30685  blof  30687  nmblore  30688  nmlnoubi  30698  nmlnogt0  30699  shsubcl  31122  unopadj  31821  atexch  32283  atcvatlem  32287  ind1  32753  ogrpsublt  33008  inelsiga  34098  inelros  34136  revpfxsfxrev  35076  mrsubcv  35470  mrsubvr  35471  btwnconn2  36063  ismtybnd  37774  lkrlsp2  39069  opcon2b  39163  opltcon2b  39172  oldmm3N  39185  oldmm4  39186  oldmj3  39189  oldmj4  39190  cmt2N  39216  cmt4N  39218  atleneN  39401  lplnri2N  39521  cdlema2N  39759  pmapojoinN  39935  ltrncnvatb  40105  trlval2  40130  trljat1  40133  cdleme18c  40260  cdleme19c  40272  cdlemeiota  40552  trlcocnv  40687  tendoplco2  40746  cdlemk6  40804  cdlemk7u  40837  cdlemk22  40860  cdlemk24-3  40870  cdlemkid2  40891  cdlemk11ta  40896  cdlemk11tc  40912  cdlemk47  40916  cdlemk52  40921  tendocnv  40988  dibelval1st1  41117  dibelval1st2N  41118  dihord2pre2  41193  mzprename  42710  pell14qrdivcl  42826  pwssplit4  43051  iocmbl  43175  relexpxpmin  43679  dvconstbi  44296  limsupgtlem  45748  dvbdfbdioolem1  45899  ibliccsinexp  45922  stoweidlem22  45993  fourierdlem42  46120  smfsuplem1  46782  divsub1dir  48479