Theorem simp1 993

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

Syntax hints:   -> wi 4   /\ w3a 974

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 976

This theorem is referenced by:  simpl1  996  simpr1  999  simp1i  1002  simp1d  1005  simp11  1023  simp21  1026  simp31  1029  syld3an3  1279  3ianorr  1305  stoic4a  1426  stoic4b  1427  rsp2e  2522  issod  4305  elirr  4526  sotri2  5010  sotri3  5011  funtpg  5251  funimaexglem  5283  feq123  5341  ftpg  5684  fsnunf  5700  foco2  5737  fcofo  5767  f1oiso2  5810  riotass  5840  ovmpox  5985  ovmpoga  5986  caovimo  6050  ofeq  6067  ofrval  6075  tfr1onlembxssdm  6326  tfrcllembxssdm  6339  frecsuclem  6389  frecrdg  6391  mapxpen  6830  diffifi  6876  unsnfidcex  6901  unsnfidcel  6902  unfidisj  6903  undifdc  6905  ssfidc  6916  iunfidisj  6927  sbthlemi9  6946  elfir  6954  djuassen  7198  mulcanenq  7351  ltanqg  7366  addnnnq0  7415  distrlem4prl  7550  distrlem4pru  7551  distrprg  7554  aptipr  7607  addsrpr  7711  mulsrpr  7712  mulasssrg  7724  ltpsrprg  7769  axmulass  7839  axpre-ltadd  7852  mul31  8054  addsubass  8133  subcan2  8148  subsub2  8151  subsub4  8156  npncan3  8161  pnpcan  8162  pnncan  8164  subcan  8178  subdi  8308  ltadd1  8352  leadd1  8353  leadd2  8354  ltsubadd  8355  lesubadd  8357  ltaddsub  8359  leaddsub  8361  lesub1  8379  lesub2  8380  ltsub1  8381  ltsub2  8382  ltaddsublt  8494  gt0add  8496  apreap  8510  lemul1  8516  reapmul1lem  8517  reapmul1  8518  reapadd1  8519  remulext1  8522  remulext2  8523  apadd2  8532  mulext2  8536  mulap0r  8538  leltap  8548  ltap  8556  apsub1  8565  recexaplem2  8574  mulcanap  8587  mulcanap2  8588  divvalap  8595  divcanap2  8601  diveqap0  8603  divrecap  8609  divrecap2  8610  divdirap  8618  divcanap3  8619  div11ap  8621  muldivdirap  8628  divcanap5  8635  redivclap  8652  div2negap  8656  apmul1  8709  apmul2  8710  div2subap  8758  ltdiv1  8788  ltmuldiv  8794  lemuldiv  8801  lt2msq1  8805  ltdiv23  8812  lediv23  8813  squeeze0  8824  difgtsumgt  9285  gtndiv  9311  eluz2  9497  eluzsub  9520  peano2uz  9546  nn01to3  9580  divge1  9684  ledivge1le  9687  addlelt  9729  xaddass  9830  xleadd1  9836  xltadd1  9837  ixxssixx  9863  lbico1  9891  lbicc2  9945  icoshftf1o  9952  fzen  10003  fzrev3  10047  fzrevral2  10066  elfzo0  10142  elfzo0z  10144  fzosplitprm1  10194  qbtwnre  10217  flqwordi  10248  flqword2  10249  adddivflid  10252  flltdivnn0lt  10264  modqcl  10286  mulqmod0  10290  modqmulnn  10302  modqabs2  10318  addmodid  10332  modifeq2int  10346  modqeqmodmin  10354  seqeq2  10409  seqeq3  10410  exp3val  10482  expnegap0  10488  expgt1  10518  exprecap  10521  leexp2a  10533  expubnd  10537  sqdivap  10544  expnbnd  10603  bccmpl  10692  fihashss  10755  leisorel  10776  shftfibg  10788  mulreap  10832  abssubne0  11059  maxleast  11181  lemininf  11201  ltmininf  11202  xrmaxltsup  11225  xrmaxaddlem  11227  xrmaxadd  11228  xrmineqinf  11236  xrltmininf  11237  xrminltinf  11239  xrminadd  11242  climuni  11260  reccn2ap  11280  isumz  11356  fsumsplitsnun  11386  geoisum1c  11487  prod1dc  11553  efltim  11665  dvdscmulr  11786  dvdsmulcr  11787  summodnegmod  11788  modmulconst  11789  dvdsmultr2  11799  dvdsexp  11825  mulmoddvds  11827  modremain  11892  divgcdz  11930  gcdaddm  11943  dvdsgcdb  11972  gcdass  11974  mulgcd  11975  gcddiv  11978  rplpwr  11986  uzwodc  11996  lcmdvdsb  12042  lcmass  12043  mulgcddvds  12052  qredeq  12054  qredeu  12055  rpmul  12056  divgcdcoprmex  12060  cncongr1  12061  rpexp  12111  rpexp12i  12113  odzcllem  12200  odzdvds  12203  odzphi  12204  pythagtriplem15  12236  pcpremul  12251  pcdiv  12260  pcqmul  12261  pcqdiv  12265  dvdsprmpweq  12292  sumhashdc  12303  pcfaclem  12305  qexpz  12308  ctinf  12389  setsvala  12451  ressid2  12481  ressval2  12482  rngbaseg  12538  grpasscan2  12767  grpidrcan  12768  grpidlcan  12769  grpinvadd  12781  grpsubeq0  12789  grppncan  12794  dfgrp3m  12802  grpsubpropd2  12808  mhmmnd  12813  mulgnegneg  12835  mulgaddcomlem  12838  mulgaddcom  12839  mulginvcom  12840  mulgmodid  12854  2basgeng  12961  clsss  12997  ntrss  12998  ntrin  13003  neiss  13029  restco  13053  restabs  13054  lmconst  13095  psmetsym  13208  psmetge0  13210  xmetge0  13244  xmetsym  13247  xmetresbl  13319  mopni3  13363  bdxmet  13380  bdmopn  13383  txmetcnp  13397  dvfvalap  13529  dvid  13541  dvcnp2cntop  13542  ptolemy  13624  rpcxpadd  13705  rpmulcxp  13709  rpdivcxp  13711  cxpmul  13712  rpcxple2  13717  rpcxplt2  13718  cxpcom  13736  rplogbval  13742  rplogbcl  13743  rprelogbmulexp  13753  relogbexpap  13755  logbleb  13758  logblt  13759  rplogbcxp  13760  rpcxplogb  13761  lgslem1  13780  lgsfcl2  13786  lgsneg  13804  lgsne0  13818  lgssq2  13821  lgsdirnn0  13827