Theorem simp1 981

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

Assertion

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

Proof of Theorem simp1

Step	Hyp	Ref	Expression
1		3simpa 978	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
2	1	simpld 111	1 |- ( ( ph /\ ps /\ ch ) -> ph )

Syntax hints:   -> wi 4   /\ w3a 962

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

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

This theorem is referenced by:  simpl1  984  simpr1  987  simp1i  990  simp1d  993  simp11  1011  simp21  1014  simp31  1017  syld3an3  1261  3ianorr  1287  stoic4a  1408  stoic4b  1409  rsp2e  2483  issod  4241  elirr  4456  sotri2  4936  sotri3  4937  funtpg  5174  funimaexglem  5206  feq123  5264  ftpg  5604  fsnunf  5620  foco2  5655  fcofo  5685  f1oiso2  5728  riotass  5757  ovmpox  5899  ovmpoga  5900  caovimo  5964  ofeq  5984  ofrval  5992  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  frecsuclem  6303  frecrdg  6305  mapxpen  6742  diffifi  6788  unsnfidcex  6808  unsnfidcel  6809  unfidisj  6810  undifdc  6812  ssfidc  6823  iunfidisj  6834  sbthlemi9  6853  elfir  6861  djuassen  7073  mulcanenq  7193  ltanqg  7208  addnnnq0  7257  distrlem4prl  7392  distrlem4pru  7393  distrprg  7396  aptipr  7449  addsrpr  7553  mulsrpr  7554  mulasssrg  7566  ltpsrprg  7611  axmulass  7681  axpre-ltadd  7694  mul31  7893  addsubass  7972  subcan2  7987  subsub2  7990  subsub4  7995  npncan3  8000  pnpcan  8001  pnncan  8003  subcan  8017  subdi  8147  ltadd1  8191  leadd1  8192  leadd2  8193  ltsubadd  8194  lesubadd  8196  ltaddsub  8198  leaddsub  8200  lesub1  8218  lesub2  8219  ltsub1  8220  ltsub2  8221  ltaddsublt  8333  gt0add  8335  apreap  8349  lemul1  8355  reapmul1lem  8356  reapmul1  8357  reapadd1  8358  remulext1  8361  remulext2  8362  apadd2  8371  mulext2  8375  mulap0r  8377  leltap  8387  ltap  8395  apsub1  8404  recexaplem2  8413  mulcanap  8426  mulcanap2  8427  divvalap  8434  divcanap2  8440  diveqap0  8442  divrecap  8448  divrecap2  8449  divdirap  8457  divcanap3  8458  div11ap  8460  muldivdirap  8467  divcanap5  8474  redivclap  8491  div2negap  8495  apmul1  8548  apmul2  8549  div2subap  8596  ltdiv1  8626  ltmuldiv  8632  lemuldiv  8639  lt2msq1  8643  ltdiv23  8650  lediv23  8651  squeeze0  8662  gtndiv  9146  eluz2  9332  eluzsub  9355  peano2uz  9378  nn01to3  9409  divge1  9510  ledivge1le  9513  addlelt  9555  xaddass  9652  xleadd1  9658  xltadd1  9659  ixxssixx  9685  lbico1  9713  lbicc2  9767  icoshftf1o  9774  fzen  9823  fzrev3  9867  fzrevral2  9886  elfzo0  9959  elfzo0z  9961  fzosplitprm1  10011  qbtwnre  10034  flqwordi  10061  flqword2  10062  adddivflid  10065  flltdivnn0lt  10077  modqcl  10099  mulqmod0  10103  modqmulnn  10115  modqabs2  10131  addmodid  10145  modifeq2int  10159  modqeqmodmin  10167  seqeq2  10222  seqeq3  10223  exp3val  10295  expnegap0  10301  expgt1  10331  exprecap  10334  leexp2a  10346  expubnd  10350  sqdivap  10357  expnbnd  10415  bccmpl  10500  fihashss  10562  leisorel  10580  shftfibg  10592  mulreap  10636  abssubne0  10863  maxleast  10985  lemininf  11005  ltmininf  11006  xrmaxltsup  11027  xrmaxaddlem  11029  xrmaxadd  11030  xrmineqinf  11038  xrltmininf  11039  xrminltinf  11041  xrminadd  11044  climuni  11062  reccn2ap  11082  isumz  11158  fsumsplitsnun  11188  geoisum1c  11289  efltim  11404  dvdscmulr  11522  dvdsmulcr  11523  summodnegmod  11524  modmulconst  11525  dvdsmultr2  11533  dvdsexp  11559  mulmoddvds  11561  modremain  11626  divgcdz  11660  gcdaddm  11672  dvdsgcdb  11701  gcdass  11703  mulgcd  11704  gcddiv  11707  rplpwr  11715  lcmdvdsb  11765  lcmass  11766  mulgcddvds  11775  qredeq  11777  qredeu  11778  rpmul  11779  divgcdcoprmex  11783  cncongr1  11784  rpexp  11831  rpexp12i  11833  ctinf  11943  setsvala  11990  ressid2  12018  ressval2  12019  rngbaseg  12075  2basgeng  12251  clsss  12287  ntrss  12288  ntrin  12293  neiss  12319  restco  12343  restabs  12344  lmconst  12385  psmetsym  12498  psmetge0  12500  xmetge0  12534  xmetsym  12537  xmetresbl  12609  mopni3  12653  bdxmet  12670  bdmopn  12673  txmetcnp  12687  dvfvalap  12819  dvid  12831  dvcnp2cntop  12832  ptolemy  12905