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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  brelrng  5941  resin  6856  moriotass  7398  omwordri  8572  oewordri  8592  dif1en  9160  dif1enOLD  9162  sdomdomtrfi  9204  php3  9212  onomeneq  9228  preleqg  9610  gchaleph2  10667  gruf  10806  nnncan1  11496  lediv1  12079  lemuldiv  12094  suprfinzcl  12676  supxrbnd  13307  bcval4  14267  ccatval3  14529  ccatfv0  14533  ccatval1lsw  14534  ccatval21sw  14535  lswccatn0lsw  14541  pfxsuff1eqwrdeq  14649  pfxccatid  14691  cshwidxmodr  14754  2swrd2eqwrdeq  14904  dvdsmultr1  16239  dvdssub2  16244  ndvdsadd  16353  mrcsscl  17564  latnle  18426  latabs1  18428  latabs2  18429  latj4rot  18443  grpsubf  18902  grpinvsub  18905  grpnpcan  18915  mulginvcom  18979  mulginvinv  18980  subgsubcl  19017  qussub  19070  ghmsub  19100  odhash3  19444  srgcom4  20037  dvrcl  20218  unitdvcl  20219  abvsubtri  20443  lspsntrim  20709  frlmsslss2  21330  lindsmm  21383  ascldimul  21442  lply1binomsc  21831  smadiadetglem2  22174  m2cpm  22243  m2cpminvid  22255  pmatcollpwscmat  22293  mp2pm2mp  22313  cpmidgsum  22370  cpmadugsumfi  22379  basgen2  22492  opnneiss  22622  restlp  22687  nmtri  24135  csschl  24893  sincosq1lem  26007  logrec  26268  nosupbnd1lem2  27212  noinfbnd1lem2  27227  noetalem1  27244  grpodivinv  29789  grpoinvdiv  29790  grpodivf  29791  nvmval2  29896  nvaddsub4  29910  nvpi  29920  nvmtri  29924  nvabs  29925  4ipval2  29961  ipval3  29962  isblo2  30036  blof  30038  nmblore  30039  nmlnoubi  30049  nmlnogt0  30050  shsubcl  30473  unopadj  31172  atexch  31634  atcvatlem  31638  ogrpsublt  32239  ind1  33015  inelsiga  33133  inelros  33171  revpfxsfxrev  34106  mrsubcv  34501  mrsubvr  34502  btwnconn2  35074  ismtybnd  36675  lkrlsp2  37973  opcon2b  38067  opltcon2b  38076  oldmm3N  38089  oldmm4  38090  oldmj3  38093  oldmj4  38094  cmt2N  38120  cmt4N  38122  atleneN  38305  lplnri2N  38425  cdlema2N  38663  pmapojoinN  38839  ltrncnvatb  39009  trlval2  39034  trljat1  39037  cdleme18c  39164  cdleme19c  39176  cdlemeiota  39456  trlcocnv  39591  tendoplco2  39650  cdlemk6  39708  cdlemk7u  39741  cdlemk22  39764  cdlemk24-3  39774  cdlemkid2  39795  cdlemk11ta  39800  cdlemk11tc  39816  cdlemk47  39820  cdlemk52  39825  tendocnv  39892  dibelval1st1  40021  dibelval1st2N  40022  dihord2pre2  40097  mzprename  41487  pell14qrdivcl  41603  pwssplit4  41831  iocmbl  41962  relexpxpmin  42468  dvconstbi  43093  limsupgtlem  44493  dvbdfbdioolem1  44644  ibliccsinexp  44667  stoweidlem22  44738  fourierdlem42  44865  smfsuplem1  45527  divsub1dir  47198