Theorem syld3an3 1409

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 1371	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  brelrng  5938  resin  6852  moriotass  7394  omwordri  8568  oewordri  8588  dif1en  9156  dif1enOLD  9158  sdomdomtrfi  9200  php3  9208  onomeneq  9224  preleqg  9606  gchaleph2  10663  gruf  10802  nnncan1  11492  lediv1  12075  lemuldiv  12090  suprfinzcl  12672  supxrbnd  13303  bcval4  14263  ccatval3  14525  ccatfv0  14529  ccatval1lsw  14530  ccatval21sw  14531  lswccatn0lsw  14537  pfxsuff1eqwrdeq  14645  pfxccatid  14687  cshwidxmodr  14750  2swrd2eqwrdeq  14900  dvdsmultr1  16235  dvdssub2  16240  ndvdsadd  16349  mrcsscl  17560  latnle  18422  latabs1  18424  latabs2  18425  latj4rot  18439  grpsubf  18898  grpinvsub  18901  grpnpcan  18911  mulginvcom  18973  mulginvinv  18974  subgsubcl  19011  qussub  19064  ghmsub  19094  odhash3  19438  srgcom4  20030  dvrcl  20210  unitdvcl  20211  abvsubtri  20435  lspsntrim  20701  frlmsslss2  21321  lindsmm  21374  ascldimul  21433  lply1binomsc  21822  smadiadetglem2  22165  m2cpm  22234  m2cpminvid  22246  pmatcollpwscmat  22284  mp2pm2mp  22304  cpmidgsum  22361  cpmadugsumfi  22370  basgen2  22483  opnneiss  22613  restlp  22678  nmtri  24126  csschl  24884  sincosq1lem  25998  logrec  26257  nosupbnd1lem2  27201  noinfbnd1lem2  27216  noetalem1  27233  grpodivinv  29776  grpoinvdiv  29777  grpodivf  29778  nvmval2  29883  nvaddsub4  29897  nvpi  29907  nvmtri  29911  nvabs  29912  4ipval2  29948  ipval3  29949  isblo2  30023  blof  30025  nmblore  30026  nmlnoubi  30036  nmlnogt0  30037  shsubcl  30460  unopadj  31159  atexch  31621  atcvatlem  31625  ogrpsublt  32226  ind1  33003  inelsiga  33121  inelros  33159  revpfxsfxrev  34094  mrsubcv  34489  mrsubvr  34490  btwnconn2  35062  ismtybnd  36663  lkrlsp2  37961  opcon2b  38055  opltcon2b  38064  oldmm3N  38077  oldmm4  38078  oldmj3  38081  oldmj4  38082  cmt2N  38108  cmt4N  38110  atleneN  38293  lplnri2N  38413  cdlema2N  38651  pmapojoinN  38827  ltrncnvatb  38997  trlval2  39022  trljat1  39025  cdleme18c  39152  cdleme19c  39164  cdlemeiota  39444  trlcocnv  39579  tendoplco2  39638  cdlemk6  39696  cdlemk7u  39729  cdlemk22  39752  cdlemk24-3  39762  cdlemkid2  39783  cdlemk11ta  39788  cdlemk11tc  39804  cdlemk47  39808  cdlemk52  39813  tendocnv  39880  dibelval1st1  40009  dibelval1st2N  40010  dihord2pre2  40085  mzprename  41472  pell14qrdivcl  41588  pwssplit4  41816  iocmbl  41947  relexpxpmin  42453  dvconstbi  43078  limsupgtlem  44479  dvbdfbdioolem1  44630  ibliccsinexp  44653  stoweidlem22  44724  fourierdlem42  44851  smfsuplem1  45513  divsub1dir  47151