Theorem syld3an3 1408

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 1135	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1370	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  5955  resin  6871  moriotass  7420  omwordri  8609  oewordri  8629  dif1en  9199  dif1enOLD  9201  sdomdomtrfi  9239  php3  9247  onomeneq  9263  preleqg  9653  gchaleph2  10710  gruf  10849  nnncan1  11543  lediv1  12131  lemuldiv  12146  suprfinzcl  12730  supxrbnd  13367  bcval4  14343  ccatval3  14614  ccatfv0  14618  ccatval1lsw  14619  ccatval21sw  14620  lswccatn0lsw  14626  pfxsuff1eqwrdeq  14734  pfxccatid  14776  cshwidxmodr  14839  2swrd2eqwrdeq  14989  dvdsmultr1  16330  dvdssub2  16335  ndvdsadd  16444  mrcsscl  17665  latnle  18531  latabs1  18533  latabs2  18534  latj4rot  18548  grpsubf  19050  grpinvsub  19053  grpnpcan  19063  mulginvcom  19130  mulginvinv  19131  subgsubcl  19168  qussub  19222  ghmsub  19255  odhash3  19609  srgcom4  20232  dvrcl  20421  unitdvcl  20422  abvsubtri  20845  lspsntrim  21115  frlmsslss2  21813  lindsmm  21866  ascldimul  21926  lply1binomsc  22331  smadiadetglem2  22694  m2cpm  22763  m2cpminvid  22775  pmatcollpwscmat  22813  mp2pm2mp  22833  cpmidgsum  22890  cpmadugsumfi  22899  basgen2  23012  opnneiss  23142  restlp  23207  nmtri  24655  csschl  25424  sincosq1lem  26554  logrec  26821  nosupbnd1lem2  27769  noinfbnd1lem2  27784  noetalem1  27801  grpodivinv  30565  grpoinvdiv  30566  grpodivf  30567  nvmval2  30672  nvaddsub4  30686  nvpi  30696  nvmtri  30700  nvabs  30701  4ipval2  30737  ipval3  30738  isblo2  30812  blof  30814  nmblore  30815  nmlnoubi  30825  nmlnogt0  30826  shsubcl  31249  unopadj  31948  atexch  32410  atcvatlem  32414  ogrpsublt  33081  ind1  33998  inelsiga  34116  inelros  34154  revpfxsfxrev  35100  mrsubcv  35495  mrsubvr  35496  btwnconn2  36084  ismtybnd  37794  lkrlsp2  39085  opcon2b  39179  opltcon2b  39188  oldmm3N  39201  oldmm4  39202  oldmj3  39205  oldmj4  39206  cmt2N  39232  cmt4N  39234  atleneN  39417  lplnri2N  39537  cdlema2N  39775  pmapojoinN  39951  ltrncnvatb  40121  trlval2  40146  trljat1  40149  cdleme18c  40276  cdleme19c  40288  cdlemeiota  40568  trlcocnv  40703  tendoplco2  40762  cdlemk6  40820  cdlemk7u  40853  cdlemk22  40876  cdlemk24-3  40886  cdlemkid2  40907  cdlemk11ta  40912  cdlemk11tc  40928  cdlemk47  40932  cdlemk52  40937  tendocnv  41004  dibelval1st1  41133  dibelval1st2N  41134  dihord2pre2  41209  mzprename  42737  pell14qrdivcl  42853  pwssplit4  43078  iocmbl  43202  relexpxpmin  43707  dvconstbi  44330  limsupgtlem  45733  dvbdfbdioolem1  45884  ibliccsinexp  45907  stoweidlem22  45978  fourierdlem42  46105  smfsuplem1  46767  divsub1dir  48363