Theorem syld3an3 1436

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  brelrng  5933  resin  6847  moriotass  7405  omwordri  8559  oewordri  8580  dif1en  9149  sdomdomtrfi  9188  php3  9196  onomeneq  9201  preleqg  9587  gchaleph2  10668  gruf  10807  nnncan1  11505  lediv1  12091  lemuldiv  12106  ind1  12238  suprfinzcl  12722  supxrbnd  13366  bcval4  14357  ccatval3  14630  ccatfv0  14635  ccatval1lsw  14636  ccatval21sw  14637  lswccatn0lsw  14644  pfxsuff1eqwrdeq  14754  pfxccatid  14796  revpfxsfxrev  14823  cshwidxmodr  14861  2swrd2eqwrdeq  15010  dvdsmultr1  16372  dvdssub2  16377  ndvdsadd  16486  mrcsscl  17694  latnle  18547  latabs1  18549  latabs2  18550  latj4rot  18564  grpsubf  19109  grpinvsub  19112  grpnpcan  19122  mulginvcom  19189  mulginvinv  19190  subgsubcl  19228  qussub  19286  ghmsub  19318  odhash3  19670  ogrpsublt  20236  srgcom4  20320  dvrcl  20512  unitdvcl  20513  abvsubtri  20960  lspsntrim  21249  frlmsslss2  21955  lindsmm  22008  ascldimul  22068  lply1binomsc  22501  smadiadetglem2  22859  m2cpm  22928  m2cpminvid  22940  pmatcollpwscmat  22978  mp2pm2mp  22998  cpmidgsum  23055  cpmadugsumfi  23064  basgen2  23176  opnneiss  23305  restlp  23370  nmtri  24814  csschl  25566  sincosq1lem  26693  logrec  26959  nosupbnd1lem2  27904  noinfbnd1lem2  27919  noetalem1  27936  grpodivinv  30935  grpoinvdiv  30936  grpodivf  30937  nvmval2  31042  nvaddsub4  31056  nvpi  31066  nvmtri  31070  nvabs  31071  4ipval2  31107  ipval3  31108  isblo2  31182  blof  31184  nmblore  31185  nmlnoubi  31195  nmlnogt0  31196  shsubcl  31619  unopadj  32318  atexch  32780  atcvatlem  32784  inelsiga  34566  inelros  34604  fineqvnttrclselem3  35569  mrsubcv  36015  mrsubvr  36016  btwnconn2  36607  ismtybnd  38491  lkrlsp2  39910  opcon2b  40004  opltcon2b  40013  oldmm3N  40026  oldmm4  40027  oldmj3  40030  oldmj4  40031  cmt2N  40057  cmt4N  40059  atleneN  40241  lplnri2N  40361  cdlema2N  40599  pmapojoinN  40775  ltrncnvatb  40945  trlval2  40970  trljat1  40973  cdleme18c  41100  cdleme19c  41112  cdlemeiota  41392  trlcocnv  41527  tendoplco2  41586  cdlemk6  41644  cdlemk7u  41677  cdlemk22  41700  cdlemk24-3  41710  cdlemkid2  41731  cdlemk11ta  41736  cdlemk11tc  41752  cdlemk47  41756  cdlemk52  41761  tendocnv  41828  dibelval1st1  41957  dibelval1st2N  41958  dihord2pre2  42033  mzprename  43513  pell14qrdivcl  43625  pwssplit4  43849  iocmbl  43973  relexpxpmin  44476  dvconstbi  45077  limsupgtlem  46524  dvbdfbdioolem1  46675  ibliccsinexp  46698  stoweidlem22  46769  fourierdlem42  46896  smfsuplem1  47558  divsub1dir  49330