Theorem syld3an3 1408

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 1135	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1370	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  brelrng  5853  resin  6747  moriotass  7274  omwordri  8412  oewordri  8432  dif1en  8954  sdomdomtrfi  8996  php3  9004  onomeneq  9020  preleqg  9382  gchaleph2  10437  gruf  10576  nnncan1  11266  lediv1  11849  lemuldiv  11864  suprfinzcl  12445  supxrbnd  13071  bcval4  14030  ccatval3  14293  ccatfv0  14297  ccatval1lsw  14298  ccatval21sw  14299  lswccatn0lsw  14305  pfxsuff1eqwrdeq  14421  pfxccatid  14463  cshwidxmodr  14526  2swrd2eqwrdeq  14675  dvdsmultr1  16014  dvdssub2  16019  ndvdsadd  16128  mrcsscl  17338  latnle  18200  latabs1  18202  latabs2  18203  latj4rot  18217  grpsubf  18663  grpinvsub  18666  grpnpcan  18676  mulginvcom  18737  mulginvinv  18738  subgsubcl  18775  qussub  18825  ghmsub  18851  odhash3  19190  dvrcl  19937  unitdvcl  19938  abvsubtri  20104  lspsntrim  20369  frlmsslss2  20991  lindsmm  21044  ascldimul  21101  lply1binomsc  21487  smadiadetglem2  21830  m2cpm  21899  m2cpminvid  21911  pmatcollpwscmat  21949  mp2pm2mp  21969  cpmidgsum  22026  cpmadugsumfi  22035  basgen2  22148  opnneiss  22278  restlp  22343  nmtri  23791  csschl  24549  sincosq1lem  25663  logrec  25922  grpodivinv  28907  grpoinvdiv  28908  grpodivf  28909  nvmval2  29014  nvaddsub4  29028  nvpi  29038  nvmtri  29042  nvabs  29043  4ipval2  29079  ipval3  29080  isblo2  29154  blof  29156  nmblore  29157  nmlnoubi  29167  nmlnogt0  29168  shsubcl  29591  unopadj  30290  atexch  30752  atcvatlem  30756  ogrpsublt  31356  ind1  31994  inelsiga  32112  inelros  32150  revpfxsfxrev  33086  mrsubcv  33481  mrsubvr  33482  nosupbnd1lem2  33921  noinfbnd1lem2  33936  noetalem1  33953  btwnconn2  34413  ismtybnd  35974  lkrlsp2  37124  opcon2b  37218  opltcon2b  37227  oldmm3N  37240  oldmm4  37241  oldmj3  37244  oldmj4  37245  cmt2N  37271  cmt4N  37273  atleneN  37455  lplnri2N  37575  cdlema2N  37813  pmapojoinN  37989  ltrncnvatb  38159  trlval2  38184  trljat1  38187  cdleme18c  38314  cdleme19c  38326  cdlemeiota  38606  trlcocnv  38741  tendoplco2  38800  cdlemk6  38858  cdlemk7u  38891  cdlemk22  38914  cdlemk24-3  38924  cdlemkid2  38945  cdlemk11ta  38950  cdlemk11tc  38966  cdlemk47  38970  cdlemk52  38975  tendocnv  39042  dibelval1st1  39171  dibelval1st2N  39172  dihord2pre2  39247  mzprename  40578  pell14qrdivcl  40694  pwssplit4  40921  iocmbl  41051  relexpxpmin  41332  dvconstbi  41959  limsupgtlem  43325  dvbdfbdioolem1  43476  ibliccsinexp  43499  stoweidlem22  43570  fourierdlem42  43697  smfsuplem1  44355  divsub1dir  45869