Theorem syld3an3 1363

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syld3an1  1364  syld3an2  1365  brelrng  5276  resin  6071  moriotass  6539  omwordri  7539  oewordri  7559  gchaleph2  9373  gruf  9512  nnncan1  10196  lediv1  10767  lemuldiv  10782  suprfinzcl  11368  supxrbnd  12030  bcval4  12956  ccatval3  13216  ccatfv0  13220  ccatval1lsw  13221  lswccatn0lsw  13226  2swrd1eqwrdeq  13306  cshwidxmodr  13401  2swrd2eqwrdeq  13544  dvdsmultr1  14857  dvdssub2  14861  ndvdsadd  14972  mrcsscl  16103  latnle  16908  latabs1  16910  latabs2  16911  latj4rot  16925  grpsubf  17317  grpinvsub  17320  grpnpcan  17330  mulginvcom  17388  mulginvinv  17389  subgsubcl  17428  qussub  17477  ghmsub  17491  odhash3  17814  dvrcl  18509  unitdvcl  18510  abvsubtri  18658  lspsntrim  18919  lply1binomsc  19498  frlmsslss2  19933  lindsmm  19986  smadiadetglem2  20297  m2cpm  20365  m2cpminvid  20377  pmatcollpwscmat  20415  mp2pm2mp  20435  cpmidgsum  20492  cpmadugsumfi  20501  basgen2  20604  opnneiss  20732  restlp  20797  nmtri  22240  sincosq1lem  24053  logrec  24301  1pthon2v  26123  grpodivinv  26774  grpoinvdiv  26775  grpodivf  26776  nvmval2  26882  nvaddsub4  26896  nvpi  26906  nvmtri  26910  nvabs  26911  4ipval2  26947  ipval3  26948  isblo2  27022  blof  27024  nmblore  27025  nmlnoubi  27035  nmlnogt0  27036  shsubcl  27461  unopadj  28162  atexch  28624  atcvatlem  28628  ogrpsublt  29053  ind1  29408  inelsiga  29525  inelros  29563  mrsubcv  30661  mrsubvr  30662  btwnconn2  31379  ismtybnd  32776  lkrlsp2  33408  opcon2b  33502  opltcon2b  33511  oldmm3N  33524  oldmm4  33525  oldmj3  33528  oldmj4  33529  cmt2N  33555  cmt4N  33557  atleneN  33738  lplnri2N  33858  cdlema2N  34096  pmapojoinN  34272  ltrncnvatb  34442  trlval2  34468  trljat1  34471  cdleme18c  34598  cdleme19c  34611  cdlemeiota  34891  trlcocnv  35026  tendoplco2  35085  cdlemk6  35143  cdlemk7u  35176  cdlemk22  35199  cdlemk24-3  35209  cdlemkid2  35230  cdlemk11ta  35235  cdlemk11tc  35251  cdlemk47  35255  cdlemk52  35260  tendocnv  35328  dibelval1st1  35457  dibelval1st2N  35458  dihord2pre2  35533  mzprename  36330  pell14qrdivcl  36447  pwssplit4  36677  iocmbl  36817  relexpxpmin  37028  dvconstbi  37555  dvbdfbdioolem1  38818  ibliccsinexp  38842  stoweidlem22  38915  fourierdlem42  39042  pfxsuff1eqwrdeq  40270  pfxccatid  40293  divsub1dir  42101