Theorem syld3an3 1437

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  brelrng  5935  resin  6877  moriotass  7440  omwordri  8618  oewordri  8639  dif1en  9215  sdomdomtrfi  9254  php3  9262  onomeneq  9267  preleqg  9653  gchaleph2  10796  gruf  10935  nnncan1  11633  lediv1  12222  lemuldiv  12237  ind1  12369  suprfinzcl  12853  supxrbnd  13498  bcval4  14492  ccatval3  14765  ccatfv0  14770  ccatval1lsw  14771  ccatval21sw  14772  lswccatn0lsw  14779  pfxsuff1eqwrdeq  14890  pfxccatid  14932  revpfxsfxrev  14959  cshwidxmodr  14997  2swrd2eqwrdeq  15149  dvdsmultr1  16510  dvdssub2  16515  ndvdsadd  16624  mrcsscl  17844  latnle  18697  latabs1  18699  latabs2  18700  latj4rot  18714  grpsubf  19279  grpinvsub  19282  grpnpcan  19292  mulginvcom  19359  mulginvinv  19360  subgsubcl  19398  qussub  19456  ghmsub  19488  odhash3  19841  ogrpsublt  20407  srgcom4  20491  dvrcl  20685  unitdvcl  20686  abvsubtri  21135  lspsntrim  21424  frlmsslss2  22136  lindsmm  22189  ascldimul  22251  lply1binomsc  22684  smadiadetglem2  23042  m2cpm  23114  m2cpminvid  23126  pmatcollpwscmat  23164  mp2pm2mp  23184  cpmidgsum  23241  cpmadugsumfi  23250  basgen2  23362  opnneiss  23491  restlp  23556  nmtri  25000  csschl  25752  sincosq1lem  26883  logrec  27148  nosupbnd1lem2  28123  noinfbnd1lem2  28138  noetalem1  28155  grpodivinv  31195  grpoinvdiv  31196  grpodivf  31197  nvmval2  31302  nvaddsub4  31316  nvpi  31326  nvmtri  31330  nvabs  31331  4ipval2  31367  ipval3  31368  isblo2  31442  blof  31444  nmblore  31445  nmlnoubi  31455  nmlnogt0  31456  shsubcl  31879  unopadj  32578  atexch  33040  atcvatlem  33044  inelsiga  34879  inelros  34917  fineqvnttrclselem3  35932  mrsubcv  36483  mrsubvr  36484  btwnconn2  37082  ismtybnd  39007  lkrlsp2  40426  opcon2b  40520  opltcon2b  40529  oldmm3N  40542  oldmm4  40543  oldmj3  40546  oldmj4  40547  cmt2N  40573  cmt4N  40575  atleneN  40757  lplnri2N  40877  cdlema2N  41115  pmapojoinN  41291  ltrncnvatb  41461  trlval2  41486  trljat1  41489  cdleme18c  41616  cdleme19c  41628  cdlemeiota  41908  trlcocnv  42043  tendoplco2  42102  cdlemk6  42160  cdlemk7u  42193  cdlemk22  42216  cdlemk24-3  42226  cdlemkid2  42247  cdlemk11ta  42252  cdlemk11tc  42268  cdlemk47  42272  cdlemk52  42277  tendocnv  42344  dibelval1st1  42473  dibelval1st2N  42474  dihord2pre2  42549  mzprename  44026  pell14qrdivcl  44138  pwssplit4  44357  iocmbl  44476  relexpxpmin  44978  dvconstbi  45579  limsupgtlem  47060  dvbdfbdioolem1  47211  ibliccsinexp  47234  stoweidlem22  47305  fourierdlem42  47432  smfsuplem1  48094  divsub1dir  49960