Theorem simp1 982

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 979	. 2 |- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
2	1	simpld 111	1 |- ( ( ph /\ ps /\ ch ) -> ph )

Syntax hints:   -> wi 4   /\ w3a 963

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 965

This theorem is referenced by:  simpl1  985  simpr1  988  simp1i  991  simp1d  994  simp11  1012  simp21  1015  simp31  1018  syld3an3  1262  3ianorr  1288  stoic4a  1409  stoic4b  1410  rsp2e  2505  issod  4274  elirr  4494  sotri2  4976  sotri3  4977  funtpg  5214  funimaexglem  5246  feq123  5304  ftpg  5644  fsnunf  5660  foco2  5695  fcofo  5725  f1oiso2  5768  riotass  5797  ovmpox  5939  ovmpoga  5940  caovimo  6004  ofeq  6024  ofrval  6032  tfr1onlembxssdm  6280  tfrcllembxssdm  6293  frecsuclem  6343  frecrdg  6345  mapxpen  6782  diffifi  6828  unsnfidcex  6853  unsnfidcel  6854  unfidisj  6855  undifdc  6857  ssfidc  6868  iunfidisj  6879  sbthlemi9  6898  elfir  6906  djuassen  7131  mulcanenq  7284  ltanqg  7299  addnnnq0  7348  distrlem4prl  7483  distrlem4pru  7484  distrprg  7487  aptipr  7540  addsrpr  7644  mulsrpr  7645  mulasssrg  7657  ltpsrprg  7702  axmulass  7772  axpre-ltadd  7785  mul31  7985  addsubass  8064  subcan2  8079  subsub2  8082  subsub4  8087  npncan3  8092  pnpcan  8093  pnncan  8095  subcan  8109  subdi  8239  ltadd1  8283  leadd1  8284  leadd2  8285  ltsubadd  8286  lesubadd  8288  ltaddsub  8290  leaddsub  8292  lesub1  8310  lesub2  8311  ltsub1  8312  ltsub2  8313  ltaddsublt  8425  gt0add  8427  apreap  8441  lemul1  8447  reapmul1lem  8448  reapmul1  8449  reapadd1  8450  remulext1  8453  remulext2  8454  apadd2  8463  mulext2  8467  mulap0r  8469  leltap  8479  ltap  8487  apsub1  8496  recexaplem2  8505  mulcanap  8518  mulcanap2  8519  divvalap  8526  divcanap2  8532  diveqap0  8534  divrecap  8540  divrecap2  8541  divdirap  8549  divcanap3  8550  div11ap  8552  muldivdirap  8559  divcanap5  8566  redivclap  8583  div2negap  8587  apmul1  8640  apmul2  8641  div2subap  8688  ltdiv1  8718  ltmuldiv  8724  lemuldiv  8731  lt2msq1  8735  ltdiv23  8742  lediv23  8743  squeeze0  8754  gtndiv  9238  eluz2  9424  eluzsub  9447  peano2uz  9473  nn01to3  9504  divge1  9608  ledivge1le  9611  addlelt  9653  xaddass  9751  xleadd1  9757  xltadd1  9758  ixxssixx  9784  lbico1  9812  lbicc2  9866  icoshftf1o  9873  fzen  9923  fzrev3  9967  fzrevral2  9986  elfzo0  10059  elfzo0z  10061  fzosplitprm1  10111  qbtwnre  10134  flqwordi  10165  flqword2  10166  adddivflid  10169  flltdivnn0lt  10181  modqcl  10203  mulqmod0  10207  modqmulnn  10219  modqabs2  10235  addmodid  10249  modifeq2int  10263  modqeqmodmin  10271  seqeq2  10326  seqeq3  10327  exp3val  10399  expnegap0  10405  expgt1  10435  exprecap  10438  leexp2a  10450  expubnd  10454  sqdivap  10461  expnbnd  10519  bccmpl  10605  fihashss  10667  leisorel  10685  shftfibg  10697  mulreap  10741  abssubne0  10968  maxleast  11090  lemininf  11110  ltmininf  11111  xrmaxltsup  11132  xrmaxaddlem  11134  xrmaxadd  11135  xrmineqinf  11143  xrltmininf  11144  xrminltinf  11146  xrminadd  11149  climuni  11167  reccn2ap  11187  isumz  11263  fsumsplitsnun  11293  geoisum1c  11394  prod1dc  11460  efltim  11572  dvdscmulr  11689  dvdsmulcr  11690  summodnegmod  11691  modmulconst  11692  dvdsmultr2  11700  dvdsexp  11726  mulmoddvds  11728  modremain  11793  divgcdz  11827  gcdaddm  11840  dvdsgcdb  11869  gcdass  11871  mulgcd  11872  gcddiv  11875  rplpwr  11883  lcmdvdsb  11933  lcmass  11934  mulgcddvds  11943  qredeq  11945  qredeu  11946  rpmul  11947  divgcdcoprmex  11951  cncongr1  11952  rpexp  11999  rpexp12i  12001  ctinf  12118  setsvala  12168  ressid2  12196  ressval2  12197  rngbaseg  12253  2basgeng  12429  clsss  12465  ntrss  12466  ntrin  12471  neiss  12497  restco  12521  restabs  12522  lmconst  12563  psmetsym  12676  psmetge0  12678  xmetge0  12712  xmetsym  12715  xmetresbl  12787  mopni3  12831  bdxmet  12848  bdmopn  12851  txmetcnp  12865  dvfvalap  12997  dvid  13009  dvcnp2cntop  13010  ptolemy  13092  rpcxpadd  13173  rpmulcxp  13177  rpdivcxp  13179  cxpmul  13180  rpcxple2  13185  rpcxplt2  13186  cxpcom  13204  rplogbval  13209  rplogbcl  13210  rprelogbmulexp  13220  relogbexpap  13222  logbleb  13225  logblt  13226  rplogbcxp  13227  rpcxplogb  13228