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  5923  resin  6845  moriotass  7407  omwordri  8573  oewordri  8594  dif1en  9170  sdomdomtrfi  9209  php3  9217  onomeneq  9222  preleqg  9609  gchaleph2  10750  gruf  10889  nnncan1  11587  lediv1  12175  lemuldiv  12190  ind1  12322  suprfinzcl  12806  supxrbnd  13451  bcval4  14444  ccatval3  14717  ccatfv0  14722  ccatval1lsw  14723  ccatval21sw  14724  lswccatn0lsw  14731  pfxsuff1eqwrdeq  14841  pfxccatid  14883  revpfxsfxrev  14910  cshwidxmodr  14948  2swrd2eqwrdeq  15099  dvdsmultr1  16459  dvdssub2  16464  ndvdsadd  16573  mrcsscl  17787  latnle  18640  latabs1  18642  latabs2  18643  latj4rot  18657  grpsubf  19222  grpinvsub  19225  grpnpcan  19235  mulginvcom  19302  mulginvinv  19303  subgsubcl  19341  qussub  19399  ghmsub  19431  odhash3  19783  ogrpsublt  20349  srgcom4  20433  dvrcl  20627  unitdvcl  20628  abvsubtri  21077  lspsntrim  21366  frlmsslss2  22074  lindsmm  22127  ascldimul  22189  lply1binomsc  22622  smadiadetglem2  22980  m2cpm  23052  m2cpminvid  23064  pmatcollpwscmat  23102  mp2pm2mp  23122  cpmidgsum  23179  cpmadugsumfi  23188  basgen2  23300  opnneiss  23429  restlp  23494  nmtri  24938  csschl  25690  sincosq1lem  26819  logrec  27084  nosupbnd1lem2  28059  noinfbnd1lem2  28074  noetalem1  28091  grpodivinv  31131  grpoinvdiv  31132  grpodivf  31133  nvmval2  31238  nvaddsub4  31252  nvpi  31262  nvmtri  31266  nvabs  31267  4ipval2  31303  ipval3  31304  isblo2  31378  blof  31380  nmblore  31381  nmlnoubi  31391  nmlnogt0  31392  shsubcl  31815  unopadj  32514  atexch  32976  atcvatlem  32980  inelsiga  34761  inelros  34799  fineqvnttrclselem3  35774  mrsubcv  36254  mrsubvr  36255  btwnconn2  36847  ismtybnd  38721  lkrlsp2  40140  opcon2b  40234  opltcon2b  40243  oldmm3N  40256  oldmm4  40257  oldmj3  40260  oldmj4  40261  cmt2N  40287  cmt4N  40289  atleneN  40471  lplnri2N  40591  cdlema2N  40829  pmapojoinN  41005  ltrncnvatb  41175  trlval2  41200  trljat1  41203  cdleme18c  41330  cdleme19c  41342  cdlemeiota  41622  trlcocnv  41757  tendoplco2  41816  cdlemk6  41874  cdlemk7u  41907  cdlemk22  41930  cdlemk24-3  41940  cdlemkid2  41961  cdlemk11ta  41966  cdlemk11tc  41982  cdlemk47  41986  cdlemk52  41991  tendocnv  42058  dibelval1st1  42187  dibelval1st2N  42188  dihord2pre2  42263  mzprename  43739  pell14qrdivcl  43851  pwssplit4  44075  iocmbl  44199  relexpxpmin  44702  dvconstbi  45303  limsupgtlem  46756  dvbdfbdioolem1  46907  ibliccsinexp  46930  stoweidlem22  47001  fourierdlem42  47128  smfsuplem1  47790  divsub1dir  49598