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  5905  resin  6822  moriotass  7376  omwordri  8536  oewordri  8556  dif1en  9124  dif1enOLD  9126  sdomdomtrfi  9165  php3  9173  onomeneq  9178  preleqg  9568  gchaleph2  10625  gruf  10764  nnncan1  11458  lediv1  12048  lemuldiv  12063  suprfinzcl  12648  supxrbnd  13288  bcval4  14272  ccatval3  14544  ccatfv0  14548  ccatval1lsw  14549  ccatval21sw  14550  lswccatn0lsw  14556  pfxsuff1eqwrdeq  14664  pfxccatid  14706  cshwidxmodr  14769  2swrd2eqwrdeq  14919  dvdsmultr1  16266  dvdssub2  16271  ndvdsadd  16380  mrcsscl  17581  latnle  18432  latabs1  18434  latabs2  18435  latj4rot  18449  grpsubf  18951  grpinvsub  18954  grpnpcan  18964  mulginvcom  19031  mulginvinv  19032  subgsubcl  19069  qussub  19123  ghmsub  19156  odhash3  19506  srgcom4  20123  dvrcl  20313  unitdvcl  20314  abvsubtri  20736  lspsntrim  21005  frlmsslss2  21684  lindsmm  21737  ascldimul  21797  lply1binomsc  22198  smadiadetglem2  22559  m2cpm  22628  m2cpminvid  22640  pmatcollpwscmat  22678  mp2pm2mp  22698  cpmidgsum  22755  cpmadugsumfi  22764  basgen2  22876  opnneiss  23005  restlp  23070  nmtri  24514  csschl  25276  sincosq1lem  26406  logrec  26673  nosupbnd1lem2  27621  noinfbnd1lem2  27636  noetalem1  27653  grpodivinv  30465  grpoinvdiv  30466  grpodivf  30467  nvmval2  30572  nvaddsub4  30586  nvpi  30596  nvmtri  30600  nvabs  30601  4ipval2  30637  ipval3  30638  isblo2  30712  blof  30714  nmblore  30715  nmlnoubi  30725  nmlnogt0  30726  shsubcl  31149  unopadj  31848  atexch  32310  atcvatlem  32314  ind1  32780  ogrpsublt  33035  inelsiga  34125  inelros  34163  revpfxsfxrev  35103  mrsubcv  35497  mrsubvr  35498  btwnconn2  36090  ismtybnd  37801  lkrlsp2  39096  opcon2b  39190  opltcon2b  39199  oldmm3N  39212  oldmm4  39213  oldmj3  39216  oldmj4  39217  cmt2N  39243  cmt4N  39245  atleneN  39428  lplnri2N  39548  cdlema2N  39786  pmapojoinN  39962  ltrncnvatb  40132  trlval2  40157  trljat1  40160  cdleme18c  40287  cdleme19c  40299  cdlemeiota  40579  trlcocnv  40714  tendoplco2  40773  cdlemk6  40831  cdlemk7u  40864  cdlemk22  40887  cdlemk24-3  40897  cdlemkid2  40918  cdlemk11ta  40923  cdlemk11tc  40939  cdlemk47  40943  cdlemk52  40948  tendocnv  41015  dibelval1st1  41144  dibelval1st2N  41145  dihord2pre2  41220  mzprename  42737  pell14qrdivcl  42853  pwssplit4  43078  iocmbl  43202  relexpxpmin  43706  dvconstbi  44323  limsupgtlem  45775  dvbdfbdioolem1  45926  ibliccsinexp  45949  stoweidlem22  46020  fourierdlem42  46147  smfsuplem1  46809  divsub1dir  48506