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

Syntax hints:   → wi 4   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  brelrng  5795  resin  6660  moriotass  7181  omwordri  8278  oewordri  8298  dif1en  8818  preleqg  9208  gchaleph2  10251  gruf  10390  nnncan1  11079  lediv1  11662  lemuldiv  11677  suprfinzcl  12257  supxrbnd  12883  bcval4  13838  ccatval3  14101  ccatfv0  14105  ccatval1lsw  14106  ccatval21sw  14107  lswccatn0lsw  14113  pfxsuff1eqwrdeq  14229  pfxccatid  14271  cshwidxmodr  14334  2swrd2eqwrdeq  14483  dvdsmultr1  15820  dvdssub2  15825  ndvdsadd  15934  mrcsscl  17077  latnle  17933  latabs1  17935  latabs2  17936  latj4rot  17950  grpsubf  18396  grpinvsub  18399  grpnpcan  18409  mulginvcom  18470  mulginvinv  18471  subgsubcl  18508  qussub  18558  ghmsub  18584  odhash3  18919  dvrcl  19658  unitdvcl  19659  abvsubtri  19825  lspsntrim  20089  frlmsslss2  20691  lindsmm  20744  ascldimul  20801  lply1binomsc  21182  smadiadetglem2  21523  m2cpm  21592  m2cpminvid  21604  pmatcollpwscmat  21642  mp2pm2mp  21662  cpmidgsum  21719  cpmadugsumfi  21728  basgen2  21840  opnneiss  21969  restlp  22034  nmtri  23478  csschl  24227  sincosq1lem  25341  logrec  25600  grpodivinv  28571  grpoinvdiv  28572  grpodivf  28573  nvmval2  28678  nvaddsub4  28692  nvpi  28702  nvmtri  28706  nvabs  28707  4ipval2  28743  ipval3  28744  isblo2  28818  blof  28820  nmblore  28821  nmlnoubi  28831  nmlnogt0  28832  shsubcl  29255  unopadj  29954  atexch  30416  atcvatlem  30420  ogrpsublt  31020  ind1  31651  inelsiga  31769  inelros  31807  revpfxsfxrev  32744  mrsubcv  33139  mrsubvr  33140  nosupbnd1lem2  33598  noinfbnd1lem2  33613  noetalem1  33630  btwnconn2  34090  ismtybnd  35651  lkrlsp2  36803  opcon2b  36897  opltcon2b  36906  oldmm3N  36919  oldmm4  36920  oldmj3  36923  oldmj4  36924  cmt2N  36950  cmt4N  36952  atleneN  37134  lplnri2N  37254  cdlema2N  37492  pmapojoinN  37668  ltrncnvatb  37838  trlval2  37863  trljat1  37866  cdleme18c  37993  cdleme19c  38005  cdlemeiota  38285  trlcocnv  38420  tendoplco2  38479  cdlemk6  38537  cdlemk7u  38570  cdlemk22  38593  cdlemk24-3  38603  cdlemkid2  38624  cdlemk11ta  38629  cdlemk11tc  38645  cdlemk47  38649  cdlemk52  38654  tendocnv  38721  dibelval1st1  38850  dibelval1st2N  38851  dihord2pre2  38926  mzprename  40215  pell14qrdivcl  40331  pwssplit4  40558  iocmbl  40688  relexpxpmin  40943  dvconstbi  41566  limsupgtlem  42936  dvbdfbdioolem1  43087  ibliccsinexp  43110  stoweidlem22  43181  fourierdlem42  43308  smfsuplem1  43959  divsub1dir  45474