Theorem simp1 999

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

Syntax hints:   -> wi 4   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  simpl1  1002  simpr1  1005  simp1i  1008  simp1d  1011  simp11  1029  simp21  1032  simp31  1035  syld3an3  1294  3ianorr  1320  stoic4a  1443  stoic4b  1444  rsp2e  2548  ifnetruedc  3602  issod  4354  elirr  4577  sotri2  5067  sotri3  5068  funtpg  5309  funimaexglem  5341  feq123  5399  ftpg  5746  fsnunf  5762  foco2  5800  fcofo  5831  f1oiso2  5874  riotass  5905  ovmpox  6051  ovmpoga  6052  caovimo  6117  ofeq  6138  ofrval  6146  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  frecsuclem  6464  frecrdg  6466  mapxpen  6909  diffifi  6955  unsnfidcex  6981  unsnfidcel  6982  unfidisj  6983  undifdc  6985  ssfidc  6998  iunfidisj  7012  sbthlemi9  7031  elfir  7039  djuassen  7284  dftap2  7318  mulcanenq  7452  ltanqg  7467  addnnnq0  7516  distrlem4prl  7651  distrlem4pru  7652  distrprg  7655  aptipr  7708  addsrpr  7812  mulsrpr  7813  mulasssrg  7825  ltpsrprg  7870  axmulass  7940  axpre-ltadd  7953  mul31  8157  addsubass  8236  subcan2  8251  subsub2  8254  subsub4  8259  npncan3  8264  pnpcan  8265  pnncan  8267  subcan  8281  subdi  8411  ltadd1  8456  leadd1  8457  leadd2  8458  ltsubadd  8459  lesubadd  8461  ltaddsub  8463  leaddsub  8465  lesub1  8483  lesub2  8484  ltsub1  8485  ltsub2  8486  ltaddsublt  8598  gt0add  8600  apreap  8614  lemul1  8620  reapmul1lem  8621  reapmul1  8622  reapadd1  8623  remulext1  8626  remulext2  8627  apadd2  8636  mulext2  8640  mulap0r  8642  leltap  8652  ltap  8660  apsub1  8669  recexaplem2  8679  mulcanap  8692  mulcanap2  8693  divvalap  8701  divcanap2  8707  diveqap0  8709  divrecap  8715  divrecap2  8716  divdirap  8724  divcanap3  8725  div11ap  8727  muldivdirap  8734  divcanap5  8741  redivclap  8758  div2negap  8762  apmul1  8815  apmul2  8816  div2subap  8864  ltdiv1  8895  ltmuldiv  8901  lemuldiv  8908  lt2msq1  8912  ltdiv23  8919  lediv23  8920  squeeze0  8931  ofnegsub  8989  difgtsumgt  9395  gtndiv  9421  eluz2  9607  eluzsub  9631  peano2uz  9657  nn01to3  9691  divge1  9798  ledivge1le  9801  addlelt  9843  xaddass  9944  xleadd1  9950  xltadd1  9951  ixxssixx  9977  lbico1  10005  lbicc2  10059  icoshftf1o  10066  fzen  10118  fzrev3  10162  fzrevral2  10181  nelfzo  10227  elfzo0  10258  elfzo0z  10260  fzosplitprm1  10310  qbtwnre  10346  flqwordi  10378  flqword2  10379  adddivflid  10382  flltdivnn0lt  10394  modqcl  10418  mulqmod0  10422  modqmulnn  10434  modqabs2  10450  addmodid  10464  modifeq2int  10478  modqeqmodmin  10486  seqeq2  10543  seqeq3  10544  seq1g  10555  seqp1g  10558  exp3val  10633  expnegap0  10639  expgt1  10669  exprecap  10672  leexp2a  10684  expubnd  10688  sqdivap  10695  expnbnd  10755  mulsubdivbinom2ap  10803  bccmpl  10846  fihashss  10908  leisorel  10929  shftfibg  10985  mulreap  11029  abssubne0  11256  maxleast  11378  lemininf  11399  ltmininf  11400  xrmaxltsup  11423  xrmaxaddlem  11425  xrmaxadd  11426  xrmineqinf  11434  xrltmininf  11435  xrminltinf  11437  xrminadd  11440  climuni  11458  reccn2ap  11478  isumz  11554  fsumsplitsnun  11584  geoisum1c  11685  prod1dc  11751  efltim  11863  dvdscmulr  11985  dvdsmulcr  11986  summodnegmod  11987  modmulconst  11988  dvdsmultr2  11998  dvdsexp  12026  mulmoddvds  12028  modremain  12094  divgcdz  12138  gcdaddm  12151  dvdsgcdb  12180  gcdass  12182  mulgcd  12183  gcddiv  12186  rplpwr  12194  uzwodc  12204  lcmdvdsb  12252  lcmass  12253  mulgcddvds  12262  qredeq  12264  qredeu  12265  rpmul  12266  divgcdcoprmex  12270  cncongr1  12271  rpexp  12321  rpexp12i  12323  odzcllem  12411  odzdvds  12414  odzphi  12415  pythagtriplem15  12447  pcpremul  12462  pcdiv  12471  pcqmul  12472  pcqdiv  12476  dvdsprmpweq  12504  sumhashdc  12516  pcfaclem  12518  qexpz  12521  ctinf  12647  setsvala  12709  ressressg  12753  ressabsg  12754  rngbaseg  12813  ptex  12935  issubmnd  13083  ress0g  13084  gsumfzz  13127  grpasscan2  13196  grpidrcan  13197  grpidlcan  13198  grpinvadd  13210  grpsubeq0  13218  grppncan  13223  dfgrp3m  13231  grpsubpropd2  13237  imasgrp2  13240  mhmmnd  13246  mulgnegneg  13271  mulgaddcomlem  13275  mulgaddcom  13276  mulginvcom  13277  mulgmodid  13291  issubg  13303  nsgconj  13336  nsgid  13345  quselbasg  13360  quseccl0g  13361  ghmnsgima  13398  cmn4  13435  ablinvadd  13440  ablsub4  13443  abladdsub4  13444  ablpncan2  13446  rngpropd  13511  imasrng  13512  issrg  13521  ringidss  13585  ringcom  13587  imasring  13620  unitmulcl  13669  unitmulclb  13670  dvrcl  13691  unitdvcl  13692  dvrcan1  13696  dvrcan3  13697  issubrng  13755  subrngpropd  13772  rrgeq0  13821  islmod  13847  lmodcom  13889  rmodislmodlem  13906  rmodislmod  13907  lss0cl  13925  lssvnegcl  13932  lssintclm  13940  lssincl  13941  lspss  13955  lspun  13958  lspsnvsi  13974  lsslsp  13985  rnglidlmmgm  14052  rnglidlmsgrp  14053  rnglidlrng  14054  qus2idrng  14081  qusmulrng  14088  2basgeng  14318  clsss  14354  ntrss  14355  ntrin  14360  neiss  14386  restco  14410  restabs  14411  lmconst  14452  psmetsym  14565  psmetge0  14567  xmetge0  14601  xmetsym  14604  xmetresbl  14676  mopni3  14720  bdxmet  14737  bdmopn  14740  txmetcnp  14754  dvfvalap  14917  dvid  14931  dvidre  14933  dvcnp2cntop  14935  elplyr  14976  ply1term  14979  ptolemy  15060  rpcxpadd  15141  rpmulcxp  15145  rpdivcxp  15147  cxpmul  15148  rpcxple2  15154  rpcxplt2  15155  cxpcom  15174  rplogbval  15181  rplogbcl  15182  rprelogbmulexp  15192  relogbexpap  15194  logbleb  15197  logblt  15198  rplogbcxp  15199  rpcxplogb  15200  sgmppw  15228  lgslem1  15241  lgsfcl2  15247  lgsneg  15265  lgsne0  15279  lgssq2  15282  lgsdirnn0  15288  gausslemma2dlem1a  15299  lgsquad  15321  2lgsoddprmlem2  15347