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  5887  resin  6793  moriotass  7344  omwordri  8496  oewordri  8516  dif1en  9082  sdomdomtrfi  9121  php3  9129  onomeneq  9134  preleqg  9516  gchaleph2  10574  gruf  10713  nnncan1  11408  lediv1  11998  lemuldiv  12013  suprfinzcl  12597  supxrbnd  13234  bcval4  14221  ccatval3  14493  ccatfv0  14498  ccatval1lsw  14499  ccatval21sw  14500  lswccatn0lsw  14506  pfxsuff1eqwrdeq  14613  pfxccatid  14655  cshwidxmodr  14718  2swrd2eqwrdeq  14867  dvdsmultr1  16214  dvdssub2  16219  ndvdsadd  16328  mrcsscl  17534  latnle  18387  latabs1  18389  latabs2  18390  latj4rot  18404  grpsubf  18940  grpinvsub  18943  grpnpcan  18953  mulginvcom  19020  mulginvinv  19021  subgsubcl  19058  qussub  19111  ghmsub  19144  odhash3  19496  ogrpsublt  20062  srgcom4  20140  dvrcl  20331  unitdvcl  20332  abvsubtri  20751  lspsntrim  21041  frlmsslss2  21721  lindsmm  21774  ascldimul  21835  lply1binomsc  22246  smadiadetglem2  22607  m2cpm  22676  m2cpminvid  22688  pmatcollpwscmat  22726  mp2pm2mp  22746  cpmidgsum  22803  cpmadugsumfi  22812  basgen2  22924  opnneiss  23053  restlp  23118  nmtri  24561  csschl  25323  sincosq1lem  26453  logrec  26720  nosupbnd1lem2  27668  noinfbnd1lem2  27683  noetalem1  27700  grpodivinv  30537  grpoinvdiv  30538  grpodivf  30539  nvmval2  30644  nvaddsub4  30658  nvpi  30668  nvmtri  30672  nvabs  30673  4ipval2  30709  ipval3  30710  isblo2  30784  blof  30786  nmblore  30787  nmlnoubi  30797  nmlnogt0  30798  shsubcl  31221  unopadj  31920  atexch  32382  atcvatlem  32386  ind1  32864  inelsiga  34220  inelros  34258  fineqvnttrclselem3  35215  revpfxsfxrev  35232  mrsubcv  35626  mrsubvr  35627  btwnconn2  36218  ismtybnd  37920  lkrlsp2  39275  opcon2b  39369  opltcon2b  39378  oldmm3N  39391  oldmm4  39392  oldmj3  39395  oldmj4  39396  cmt2N  39422  cmt4N  39424  atleneN  39606  lplnri2N  39726  cdlema2N  39964  pmapojoinN  40140  ltrncnvatb  40310  trlval2  40335  trljat1  40338  cdleme18c  40465  cdleme19c  40477  cdlemeiota  40757  trlcocnv  40892  tendoplco2  40951  cdlemk6  41009  cdlemk7u  41042  cdlemk22  41065  cdlemk24-3  41075  cdlemkid2  41096  cdlemk11ta  41101  cdlemk11tc  41117  cdlemk47  41121  cdlemk52  41126  tendocnv  41193  dibelval1st1  41322  dibelval1st2N  41323  dihord2pre2  41398  mzprename  42906  pell14qrdivcl  43022  pwssplit4  43246  iocmbl  43370  relexpxpmin  43874  dvconstbi  44491  limsupgtlem  45937  dvbdfbdioolem1  46088  ibliccsinexp  46111  stoweidlem22  46182  fourierdlem42  46309  smfsuplem1  46971  divsub1dir  48679