Theorem syld3an3 1411

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 1373	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  brelrng  5890  resin  6796  moriotass  7347  omwordri  8499  oewordri  8520  dif1en  9086  sdomdomtrfi  9125  php3  9133  onomeneq  9138  preleqg  9524  gchaleph2  10583  gruf  10722  nnncan1  11417  lediv1  12007  lemuldiv  12022  suprfinzcl  12606  supxrbnd  13243  bcval4  14230  ccatval3  14502  ccatfv0  14507  ccatval1lsw  14508  ccatval21sw  14509  lswccatn0lsw  14515  pfxsuff1eqwrdeq  14622  pfxccatid  14664  cshwidxmodr  14727  2swrd2eqwrdeq  14876  dvdsmultr1  16223  dvdssub2  16228  ndvdsadd  16337  mrcsscl  17543  latnle  18396  latabs1  18398  latabs2  18399  latj4rot  18413  grpsubf  18949  grpinvsub  18952  grpnpcan  18962  mulginvcom  19029  mulginvinv  19030  subgsubcl  19067  qussub  19120  ghmsub  19153  odhash3  19505  ogrpsublt  20071  srgcom4  20149  dvrcl  20340  unitdvcl  20341  abvsubtri  20760  lspsntrim  21050  frlmsslss2  21730  lindsmm  21783  ascldimul  21844  lply1binomsc  22255  smadiadetglem2  22616  m2cpm  22685  m2cpminvid  22697  pmatcollpwscmat  22735  mp2pm2mp  22755  cpmidgsum  22812  cpmadugsumfi  22821  basgen2  22933  opnneiss  23062  restlp  23127  nmtri  24570  csschl  25332  sincosq1lem  26462  logrec  26729  nosupbnd1lem2  27677  noinfbnd1lem2  27692  noetalem1  27709  grpodivinv  30611  grpoinvdiv  30612  grpodivf  30613  nvmval2  30718  nvaddsub4  30732  nvpi  30742  nvmtri  30746  nvabs  30747  4ipval2  30783  ipval3  30784  isblo2  30858  blof  30860  nmblore  30861  nmlnoubi  30871  nmlnogt0  30872  shsubcl  31295  unopadj  31994  atexch  32456  atcvatlem  32460  ind1  32936  inelsiga  34292  inelros  34330  fineqvnttrclselem3  35279  revpfxsfxrev  35310  mrsubcv  35704  mrsubvr  35705  btwnconn2  36296  ismtybnd  38008  lkrlsp2  39363  opcon2b  39457  opltcon2b  39466  oldmm3N  39479  oldmm4  39480  oldmj3  39483  oldmj4  39484  cmt2N  39510  cmt4N  39512  atleneN  39694  lplnri2N  39814  cdlema2N  40052  pmapojoinN  40228  ltrncnvatb  40398  trlval2  40423  trljat1  40426  cdleme18c  40553  cdleme19c  40565  cdlemeiota  40845  trlcocnv  40980  tendoplco2  41039  cdlemk6  41097  cdlemk7u  41130  cdlemk22  41153  cdlemk24-3  41163  cdlemkid2  41184  cdlemk11ta  41189  cdlemk11tc  41205  cdlemk47  41209  cdlemk52  41214  tendocnv  41281  dibelval1st1  41410  dibelval1st2N  41411  dihord2pre2  41486  mzprename  42991  pell14qrdivcl  43107  pwssplit4  43331  iocmbl  43455  relexpxpmin  43958  dvconstbi  44575  limsupgtlem  46021  dvbdfbdioolem1  46172  ibliccsinexp  46195  stoweidlem22  46266  fourierdlem42  46393  smfsuplem1  47055  divsub1dir  48763