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  5887  resin  6790  moriotass  7342  omwordri  8497  oewordri  8517  dif1en  9084  dif1enOLD  9086  sdomdomtrfi  9125  php3  9133  onomeneq  9138  preleqg  9530  gchaleph2  10585  gruf  10724  nnncan1  11419  lediv1  12009  lemuldiv  12024  suprfinzcl  12609  supxrbnd  13249  bcval4  14233  ccatval3  14505  ccatfv0  14509  ccatval1lsw  14510  ccatval21sw  14511  lswccatn0lsw  14517  pfxsuff1eqwrdeq  14624  pfxccatid  14666  cshwidxmodr  14729  2swrd2eqwrdeq  14879  dvdsmultr1  16226  dvdssub2  16231  ndvdsadd  16340  mrcsscl  17545  latnle  18398  latabs1  18400  latabs2  18401  latj4rot  18415  grpsubf  18917  grpinvsub  18920  grpnpcan  18930  mulginvcom  18997  mulginvinv  18998  subgsubcl  19035  qussub  19089  ghmsub  19122  odhash3  19474  ogrpsublt  20040  srgcom4  20118  dvrcl  20308  unitdvcl  20309  abvsubtri  20731  lspsntrim  21021  frlmsslss2  21701  lindsmm  21754  ascldimul  21814  lply1binomsc  22215  smadiadetglem2  22576  m2cpm  22645  m2cpminvid  22657  pmatcollpwscmat  22695  mp2pm2mp  22715  cpmidgsum  22772  cpmadugsumfi  22781  basgen2  22893  opnneiss  23022  restlp  23087  nmtri  24531  csschl  25293  sincosq1lem  26423  logrec  26690  nosupbnd1lem2  27638  noinfbnd1lem2  27653  noetalem1  27670  grpodivinv  30499  grpoinvdiv  30500  grpodivf  30501  nvmval2  30606  nvaddsub4  30620  nvpi  30630  nvmtri  30634  nvabs  30635  4ipval2  30671  ipval3  30672  isblo2  30746  blof  30748  nmblore  30749  nmlnoubi  30759  nmlnogt0  30760  shsubcl  31183  unopadj  31882  atexch  32344  atcvatlem  32348  ind1  32819  inelsiga  34121  inelros  34159  revpfxsfxrev  35108  mrsubcv  35502  mrsubvr  35503  btwnconn2  36095  ismtybnd  37806  lkrlsp2  39101  opcon2b  39195  opltcon2b  39204  oldmm3N  39217  oldmm4  39218  oldmj3  39221  oldmj4  39222  cmt2N  39248  cmt4N  39250  atleneN  39433  lplnri2N  39553  cdlema2N  39791  pmapojoinN  39967  ltrncnvatb  40137  trlval2  40162  trljat1  40165  cdleme18c  40292  cdleme19c  40304  cdlemeiota  40584  trlcocnv  40719  tendoplco2  40778  cdlemk6  40836  cdlemk7u  40869  cdlemk22  40892  cdlemk24-3  40902  cdlemkid2  40923  cdlemk11ta  40928  cdlemk11tc  40944  cdlemk47  40948  cdlemk52  40953  tendocnv  41020  dibelval1st1  41149  dibelval1st2N  41150  dihord2pre2  41225  mzprename  42742  pell14qrdivcl  42858  pwssplit4  43082  iocmbl  43206  relexpxpmin  43710  dvconstbi  44327  limsupgtlem  45778  dvbdfbdioolem1  45929  ibliccsinexp  45952  stoweidlem22  46023  fourierdlem42  46150  smfsuplem1  46812  divsub1dir  48522