Theorem syld3an3 1434

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  brelrng  5929  resin  6841  moriotass  7397  omwordri  8553  oewordri  8574  dif1en  9142  sdomdomtrfi  9181  php3  9189  onomeneq  9194  preleqg  9580  gchaleph2  10653  gruf  10792  nnncan1  11490  lediv1  12076  lemuldiv  12091  ind1  12223  suprfinzcl  12706  supxrbnd  13350  bcval4  14339  ccatval3  14612  ccatfv0  14617  ccatval1lsw  14618  ccatval21sw  14619  lswccatn0lsw  14625  pfxsuff1eqwrdeq  14732  pfxccatid  14774  cshwidxmodr  14837  2swrd2eqwrdeq  14986  dvdsmultr1  16350  dvdssub2  16355  ndvdsadd  16464  mrcsscl  17672  latnle  18525  latabs1  18527  latabs2  18528  latj4rot  18542  grpsubf  19081  grpinvsub  19084  grpnpcan  19094  mulginvcom  19161  mulginvinv  19162  subgsubcl  19200  qussub  19258  ghmsub  19290  odhash3  19642  ogrpsublt  20208  srgcom4  20292  dvrcl  20482  unitdvcl  20483  abvsubtri  20904  lspsntrim  21193  frlmsslss2  21890  lindsmm  21943  ascldimul  22003  lply1binomsc  22436  smadiadetglem2  22794  m2cpm  22863  m2cpminvid  22875  pmatcollpwscmat  22913  mp2pm2mp  22933  cpmidgsum  22990  cpmadugsumfi  22999  basgen2  23111  opnneiss  23240  restlp  23305  nmtri  24748  csschl  25500  sincosq1lem  26624  logrec  26890  nosupbnd1lem2  27835  noinfbnd1lem2  27850  noetalem1  27867  grpodivinv  30825  grpoinvdiv  30826  grpodivf  30827  nvmval2  30932  nvaddsub4  30946  nvpi  30956  nvmtri  30960  nvabs  30961  4ipval2  30997  ipval3  30998  isblo2  31072  blof  31074  nmblore  31075  nmlnoubi  31085  nmlnogt0  31086  shsubcl  31509  unopadj  32208  atexch  32670  atcvatlem  32674  inelsiga  34466  inelros  34504  fineqvnttrclselem3  35455  revpfxsfxrev  35502  mrsubcv  35897  mrsubvr  35898  btwnconn2  36489  ismtybnd  38341  lkrlsp2  39762  opcon2b  39856  opltcon2b  39865  oldmm3N  39878  oldmm4  39879  oldmj3  39882  oldmj4  39883  cmt2N  39909  cmt4N  39911  atleneN  40093  lplnri2N  40213  cdlema2N  40451  pmapojoinN  40627  ltrncnvatb  40797  trlval2  40822  trljat1  40825  cdleme18c  40952  cdleme19c  40964  cdlemeiota  41244  trlcocnv  41379  tendoplco2  41438  cdlemk6  41496  cdlemk7u  41529  cdlemk22  41552  cdlemk24-3  41562  cdlemkid2  41583  cdlemk11ta  41588  cdlemk11tc  41604  cdlemk47  41608  cdlemk52  41613  tendocnv  41680  dibelval1st1  41809  dibelval1st2N  41810  dihord2pre2  41885  mzprename  43367  pell14qrdivcl  43479  pwssplit4  43703  iocmbl  43827  relexpxpmin  44330  dvconstbi  44931  limsupgtlem  46378  dvbdfbdioolem1  46529  ibliccsinexp  46552  stoweidlem22  46623  fourierdlem42  46750  smfsuplem1  47412  divsub1dir  49177