Theorem syld3an3 1400

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

Syntax hints:   → wi 4   ∧ w3a 1078

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 208  df-an 397  df-3an 1080

This theorem is referenced by:  brelrng  5685  resin  6496  moriotass  6997  omwordri  8039  oewordri  8059  preleqg  8913  gchaleph2  9929  gruf  10068  nnncan1  10759  lediv1  11342  lemuldiv  11357  suprfinzcl  11935  supxrbnd  12560  bcval4  13505  ccatval3  13765  ccatfv0  13769  ccatval1lsw  13770  ccatval21sw  13771  lswccatn0lsw  13777  pfxsuff1eqwrdeq  13885  pfxccatid  13927  cshwidxmodr  13990  2swrd2eqwrdeq  14139  dvdsmultr1  15468  dvdssub2  15472  ndvdsadd  15582  mrcsscl  16708  latnle  17512  latabs1  17514  latabs2  17515  latj4rot  17529  grpsubf  17923  grpinvsub  17926  grpnpcan  17936  mulginvcom  17994  mulginvinv  17995  subgsubcl  18032  qussub  18081  ghmsub  18095  odhash3  18419  dvrcl  19114  unitdvcl  19115  abvsubtri  19284  lspsntrim  19548  ascldimul  19792  lply1binomsc  20146  frlmsslss2  20589  lindsmm  20642  smadiadetglem2  20953  m2cpm  21021  m2cpminvid  21033  pmatcollpwscmat  21071  mp2pm2mp  21091  cpmidgsum  21148  cpmadugsumfi  21157  basgen2  21269  opnneiss  21398  restlp  21463  nmtri  22906  csschl  23650  sincosq1lem  24754  logrec  25010  grpodivinv  27992  grpoinvdiv  27993  grpodivf  27994  nvmval2  28099  nvaddsub4  28113  nvpi  28123  nvmtri  28127  nvabs  28128  4ipval2  28164  ipval3  28165  isblo2  28239  blof  28241  nmblore  28242  nmlnoubi  28252  nmlnogt0  28253  shsubcl  28676  unopadj  29375  atexch  29837  atcvatlem  29841  ogrpsublt  30352  ind1  30849  inelsiga  30967  inelros  31005  mrsubcv  32310  mrsubvr  32311  nosupbnd1lem2  32763  btwnconn2  33117  ismtybnd  34563  lkrlsp2  35720  opcon2b  35814  opltcon2b  35823  oldmm3N  35836  oldmm4  35837  oldmj3  35840  oldmj4  35841  cmt2N  35867  cmt4N  35869  atleneN  36051  lplnri2N  36171  cdlema2N  36409  pmapojoinN  36585  ltrncnvatb  36755  trlval2  36780  trljat1  36783  cdleme18c  36910  cdleme19c  36922  cdlemeiota  37202  trlcocnv  37337  tendoplco2  37396  cdlemk6  37454  cdlemk7u  37487  cdlemk22  37510  cdlemk24-3  37520  cdlemkid2  37541  cdlemk11ta  37546  cdlemk11tc  37562  cdlemk47  37566  cdlemk52  37571  tendocnv  37638  dibelval1st1  37767  dibelval1st2N  37768  dihord2pre2  37843  mzprename  38781  pell14qrdivcl  38898  pwssplit4  39125  iocmbl  39255  relexpxpmin  39498  dvconstbi  40156  limsupgtlem  41554  dvbdfbdioolem1  41708  ibliccsinexp  41731  stoweidlem22  41803  fourierdlem42  41930  smfsuplem1  42581  divsub1dir  44007