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  5925  resin  6840  moriotass  7402  omwordri  8559  oewordri  8580  dif1en  9156  sdomdomtrfi  9195  php3  9203  onomeneq  9208  preleqg  9594  gchaleph2  10681  gruf  10820  nnncan1  11518  lediv1  12104  lemuldiv  12119  ind1  12251  suprfinzcl  12735  supxrbnd  13380  bcval4  14371  ccatval3  14644  ccatfv0  14649  ccatval1lsw  14650  ccatval21sw  14651  lswccatn0lsw  14658  pfxsuff1eqwrdeq  14768  pfxccatid  14810  revpfxsfxrev  14837  cshwidxmodr  14875  2swrd2eqwrdeq  15026  dvdsmultr1  16386  dvdssub2  16391  ndvdsadd  16500  mrcsscl  17708  latnle  18561  latabs1  18563  latabs2  18564  latj4rot  18578  grpsubf  19142  grpinvsub  19145  grpnpcan  19155  mulginvcom  19222  mulginvinv  19223  subgsubcl  19261  qussub  19319  ghmsub  19351  odhash3  19703  ogrpsublt  20269  srgcom4  20353  dvrcl  20545  unitdvcl  20546  abvsubtri  20993  lspsntrim  21282  frlmsslss2  21988  lindsmm  22041  ascldimul  22103  lply1binomsc  22536  smadiadetglem2  22894  m2cpm  22966  m2cpminvid  22978  pmatcollpwscmat  23016  mp2pm2mp  23036  cpmidgsum  23093  cpmadugsumfi  23102  basgen2  23214  opnneiss  23343  restlp  23408  nmtri  24852  csschl  25604  sincosq1lem  26735  logrec  27000  nosupbnd1lem2  27945  noinfbnd1lem2  27960  noetalem1  27977  grpodivinv  31017  grpoinvdiv  31018  grpodivf  31019  nvmval2  31124  nvaddsub4  31138  nvpi  31148  nvmtri  31152  nvabs  31153  4ipval2  31189  ipval3  31190  isblo2  31264  blof  31266  nmblore  31267  nmlnoubi  31277  nmlnogt0  31278  shsubcl  31701  unopadj  32400  atexch  32862  atcvatlem  32866  inelsiga  34646  inelros  34684  fineqvnttrclselem3  35649  mrsubcv  36089  mrsubvr  36090  btwnconn2  36682  ismtybnd  38557  lkrlsp2  39976  opcon2b  40070  opltcon2b  40079  oldmm3N  40092  oldmm4  40093  oldmj3  40096  oldmj4  40097  cmt2N  40123  cmt4N  40125  atleneN  40307  lplnri2N  40427  cdlema2N  40665  pmapojoinN  40841  ltrncnvatb  41011  trlval2  41036  trljat1  41039  cdleme18c  41166  cdleme19c  41178  cdlemeiota  41458  trlcocnv  41593  tendoplco2  41652  cdlemk6  41710  cdlemk7u  41743  cdlemk22  41766  cdlemk24-3  41776  cdlemkid2  41797  cdlemk11ta  41802  cdlemk11tc  41818  cdlemk47  41822  cdlemk52  41827  tendocnv  41894  dibelval1st1  42023  dibelval1st2N  42024  dihord2pre2  42099  mzprename  43594  pell14qrdivcl  43706  pwssplit4  43930  iocmbl  44054  relexpxpmin  44557  dvconstbi  45158  limsupgtlem  46605  dvbdfbdioolem1  46756  ibliccsinexp  46779  stoweidlem22  46850  fourierdlem42  46977  smfsuplem1  47639  divsub1dir  49447