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 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  brelrng  5931  resin  6843  moriotass  7399  omwordri  8553  oewordri  8574  dif1en  9142  sdomdomtrfi  9181  php3  9189  onomeneq  9194  preleqg  9580  gchaleph2  10652  gruf  10791  nnncan1  11489  lediv1  12075  lemuldiv  12090  ind1  12222  suprfinzcl  12705  supxrbnd  13349  bcval4  14339  ccatval3  14612  ccatfv0  14617  ccatval1lsw  14618  ccatval21sw  14619  lswccatn0lsw  14625  pfxsuff1eqwrdeq  14732  pfxccatid  14774  cshwidxmodr  14837  2swrd2eqwrdeq  14986  dvdsmultr1  16349  dvdssub2  16354  ndvdsadd  16463  mrcsscl  17671  latnle  18524  latabs1  18526  latabs2  18527  latj4rot  18541  grpsubf  19080  grpinvsub  19083  grpnpcan  19093  mulginvcom  19160  mulginvinv  19161  subgsubcl  19199  qussub  19257  ghmsub  19289  odhash3  19641  ogrpsublt  20207  srgcom4  20291  dvrcl  20482  unitdvcl  20483  abvsubtri  20930  lspsntrim  21219  frlmsslss2  21925  lindsmm  21978  ascldimul  22038  lply1binomsc  22471  smadiadetglem2  22829  m2cpm  22898  m2cpminvid  22910  pmatcollpwscmat  22948  mp2pm2mp  22968  cpmidgsum  23025  cpmadugsumfi  23034  basgen2  23146  opnneiss  23275  restlp  23340  nmtri  24783  csschl  25535  sincosq1lem  26662  logrec  26928  nosupbnd1lem2  27873  noinfbnd1lem2  27888  noetalem1  27905  grpodivinv  30888  grpoinvdiv  30889  grpodivf  30890  nvmval2  30995  nvaddsub4  31009  nvpi  31019  nvmtri  31023  nvabs  31024  4ipval2  31060  ipval3  31061  isblo2  31135  blof  31137  nmblore  31138  nmlnoubi  31148  nmlnogt0  31149  shsubcl  31572  unopadj  32271  atexch  32733  atcvatlem  32737  inelsiga  34525  inelros  34563  fineqvnttrclselem3  35536  revpfxsfxrev  35607  mrsubcv  36002  mrsubvr  36003  btwnconn2  36594  ismtybnd  38458  lkrlsp2  39877  opcon2b  39971  opltcon2b  39980  oldmm3N  39993  oldmm4  39994  oldmj3  39997  oldmj4  39998  cmt2N  40024  cmt4N  40026  atleneN  40208  lplnri2N  40328  cdlema2N  40566  pmapojoinN  40742  ltrncnvatb  40912  trlval2  40937  trljat1  40940  cdleme18c  41067  cdleme19c  41079  cdlemeiota  41359  trlcocnv  41494  tendoplco2  41553  cdlemk6  41611  cdlemk7u  41644  cdlemk22  41667  cdlemk24-3  41677  cdlemkid2  41698  cdlemk11ta  41703  cdlemk11tc  41719  cdlemk47  41723  cdlemk52  41728  tendocnv  41795  dibelval1st1  41924  dibelval1st2N  41925  dihord2pre2  42000  mzprename  43480  pell14qrdivcl  43592  pwssplit4  43816  iocmbl  43940  relexpxpmin  44443  dvconstbi  45044  limsupgtlem  46491  dvbdfbdioolem1  46642  ibliccsinexp  46665  stoweidlem22  46736  fourierdlem42  46863  smfsuplem1  47525  divsub1dir  49297