Theorem simp3 994

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp3	|- ( ( ph /\ ps /\ ch ) -> ch )

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 991	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )
2	1	simprd 113	1 |- ( ( ph /\ ps /\ ch ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  simpl3  997  simpr3  1000  simp3i  1003  simp3d  1006  simp13  1024  simp23  1027  simp33  1030  3anibar  1160  3ianorr  1304  stoic4a  1425  stoic4b  1426  mob2  2910  sotri2  5008  sotri3  5009  feq123  5339  resasplitss  5377  sefvex  5517  ftpg  5680  fsnunf  5696  fnfvima  5730  cocan1  5766  cocan2  5767  f1oiso2  5806  riotass  5836  moriotass  5837  ovmpox  5981  ovmpoga  5982  caovimo  6046  ofrval  6071  dfsmo2  6266  tfr1onlembfn  6323  tfrcllembfn  6336  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecrdg  6387  nnsucsssuc  6471  f1oen2g  6733  f1dom2g  6734  xpdom3m  6812  mapxpen  6826  diffifi  6872  unfidisj  6899  undifdc  6901  ssfidc  6912  sbthlemi9  6942  ctssdc  7090  endjudisj  7187  djuassen  7194  xpdjuen  7195  mulcanenq  7347  ltanqg  7362  addnnnq0  7411  nnanq0  7420  prltlu  7449  distrprg  7550  ltexprlemm  7562  recexprlem1ssl  7595  recexprlem1ssu  7596  addsrpr  7707  mulsrpr  7708  mulasssrg  7720  recexgt0sr  7735  ltpsrprg  7765  axmulass  7835  axpre-ltadd  7848  ltxrlt  7985  subadd2  8123  addsubass  8129  nppcan  8141  nppcan3  8143  subcan2  8144  subsub2  8147  subsub4  8152  pnpcan  8158  pnncan  8160  subcan  8174  subdi  8304  ltadd1  8348  leadd1  8349  leadd2  8350  ltsubadd  8351  ltsubadd2  8352  lesubadd  8353  lesubadd2  8354  ltaddsub  8355  leaddsub  8357  lesub1  8375  lesub2  8376  ltsub1  8377  ltsub2  8378  ltaddsublt  8490  gt0add  8492  reapadd1  8515  remulext1  8518  remulext2  8519  apadd2  8528  mulext2  8532  mulap0r  8534  leltap  8544  ltap  8552  apsub1  8561  divap0b  8600  divmulasscomap  8613  divcanap5  8631  dmdcanap  8639  redivclap  8648  div2negap  8652  lt2msq1  8801  ltdiv2  8803  nndivtr  8920  difgtsumgt  9281  gtndiv  9307  eluzsub  9516  nn01to3  9576  qdivcl  9602  irrmul  9606  rpgecl  9639  divge1  9680  xaddass  9826  xltadd1  9833  ubioog  9871  ubioc1  9886  lbico1  9887  iccleub  9888  lbicc2  9941  ubicc2  9942  icoshftf1o  9948  fzen  9999  elfz1b  10046  uznfz  10059  elfzo0  10138  elfzo0z  10140  ubmelfzo  10156  fzonn0p1p1  10169  ubmelm1fzo  10182  qbtwnre  10213  flqwordi  10244  flltdivnn0lt  10260  ceiqle  10269  modqval  10280  modqvalr  10281  modqcl  10282  flqpmodeq  10283  modq0  10285  mulqmod0  10286  negqmod0  10287  modqge0  10288  modqlt  10289  modqdiffl  10291  modqdifz  10292  modqmulnn  10298  modqvalp1  10299  modqabs2  10314  modqmuladdnn0  10324  qnegmod  10325  addmodid  10328  modqeqmodmin  10350  modfzo0difsn  10351  addmodlteq  10354  frec2uzf1od  10362  expnegap0  10484  expgt1  10514  exprecap  10517  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  mulbinom2  10592  expnbnd  10599  fihashss  10751  fimaxq  10762  seq3coll  10777  shftfibg  10784  redivap  10838  imdivap  10845  cjdivap  10873  maxleast  11177  lemininf  11197  ltmininf  11198  bdtrilem  11202  bdtri  11203  xrmaxaddlem  11223  xrmaxadd  11224  xrmineqinf  11232  xrltmininf  11233  xrminltinf  11235  xrminadd  11238  climuni  11256  reccn2ap  11276  isumz  11352  fsumsplitsnun  11382  geoisum1c  11483  prodfap0  11508  prod1dc  11549  fprodabs  11579  cos12dec  11730  summodnegmod  11784  dvdsmultr2  11795  mulmoddvds  11823  divalglemeuneg  11882  zsupssdc  11909  gcdaddm  11939  gcdass  11970  mulgcd  11971  gcddiv  11974  nnminle  11990  lcmass  12039  mulgcddvds  12048  qredeq  12050  congr  12054  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  prmexpb  12105  rpexp  12107  pythagtriplem1  12219  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem12  12229  pythagtriplem13  12230  pythagtriplem15  12232  pythagtriplem19  12236  pcdiv  12256  dvdsprmpweqle  12290  sumhashdc  12299  pcbc  12303  unennn  12352  nninfdc  12408  fvsetsid  12450  ressid2  12477  ressval2  12478  rngmulrg  12536  mgmsscl  12615  plusfvalg  12617  grpasscan2  12763  grpidrcan  12764  grpidlcan  12765  basgen  12874  2basgeng  12876  ntrss  12913  neiss  12944  opnneiss  12952  restco  12968  restabs  12969  cnprcl2k  13000  cnpf2  13001  lmconst  13010  cnpnei  13013  cnptoprest  13033  cnmpt2t  13087  psmetsym  13123  psmetge0  13125  xmetge0  13159  xmetsym  13162  blvalps  13182  blval  13183  ssblps  13219  ssbl  13220  blpnfctr  13233  xmssym  13263  bdxmet  13295  metcnp3  13305  dvfvalap  13444  dvid  13456  dvcnp2cntop  13457  ptolemy  13539  rpcxpadd  13620  rpcxpsub  13623  rpmulcxp  13624  cxpmul  13627  rpcxple2  13632  rpcxplt2  13633  cxpcom  13651  rplogbval  13657  rplogbcl  13658  rplogbchbase  13662  rplogbreexp  13665  relogbexpap  13670  logbleb  13673  logblt  13674  rplogbcxp  13675  rpcxplogb  13676  relogbcxpbap  13677  lgslem1  13695  lgsfvalg  13700  lgsval4  13715  lgsneg  13719  lgsne0  13733  lgsdinn0  13743