Theorem simpld 112

Description: Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
simpld.1	|- ( ph -> ( ps /\ ch ) )

Assertion

Ref	Expression
simpld	|- ( ph -> ps )

Proof of Theorem simpld

Step	Hyp	Ref	Expression
1		simpld.1	. 2 |- ( ph -> ( ps /\ ch ) )
2		simpl 109	. 2 |- ( ( ps /\ ch ) -> ps )
3	1, 2	syl 14	1 |- ( ph -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem is used by:  biimp  118  simplbi  274  simprbda  383  simplld  532  simplrd  534  simprld  536  simp1  1028  eldifad  3231  unssad  3406  opth1  4376  opth  4377  0nelop  4388  epelg  4435  poirr  4452  brrelex1  4814  brrelex  4815  asymref  5173  soirri  5182  sotri  5183  ffdmd  5559  fcnvres  5575  fun11iun  5660  funopsn  5891  elmpocl1  6285  f1od  6293  f1o2d  6295  oprssdmm  6405  elmpom  6474  fczsupp0  6499  smoiso  6573  tfrlem1  6579  swoer  6835  ecopovtrn  6906  ecopovtrng  6909  elmapssres  6954  pmresg  6957  mapsspm  6963  en1uniel  7091  pw2f1odc  7135  xpf1o  7144  sbthlemi9  7282  fsuppfund  7294  supelti  7343  supsnti  7346  supisoti  7351  ctssdccl  7452  ctfoex  7459  fodjum  7487  en2eleq  7548  djuen  7568  pw1if  7585  dftap2  7618  2omotaplemst  7625  exmidapne  7627  ccfunen  7631  dfplpq2  7722  ltbtwnnqq  7783  enq0tr  7802  elnp1st2nd  7844  prcdnql  7852  prnminu  7857  prloc  7859  genpcdl  7887  addnqprulem  7896  addlocprlemlt  7899  addlocprlemgt  7902  addlocprlem  7903  addlocpr  7904  nqprxx  7914  ltnqex  7917  addnqprlemfl  7927  addnqprlemfu  7928  appdivnq  7931  prmuloclemcalc  7933  prmuloc  7934  mullocprlem  7938  mulnqprlemfl  7943  mulnqprlemfu  7944  ltprordil  7957  ltnqpri  7962  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemrl  7978  ltexprlemfu  7979  ltexprlemru  7980  ltexpri  7981  lteupri  7985  ltaprlem  7986  recexprlemell  7990  recexprlemelu  7991  recexprlemloc  7999  recexprlempr  8000  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1u  8004  aptipr  8009  cauappcvgprlemm  8013  cauappcvgprlemlol  8015  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlem1  8027  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemlol  8038  caucvgprlemladdfu  8045  caucvgprprlemloccalc  8052  caucvgprprlemnkltj  8057  caucvgprprlemnbj  8061  caucvgprprlemml  8062  caucvgprprlemlol  8066  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  suplocexprlemss  8083  suplocexprlemru  8087  suplocexprlemlub  8092  ltsrprg  8115  caucvgsrlemasr  8158  suplocsrlemb  8174  suplocsrlem  8176  suplocsr  8177  axcaucvglemcau  8266  axpre-suploclemres  8269  negf1o  8711  apreap  8918  apreim  8934  msqge0  8947  mulge0  8950  apti  8953  apsscn  8978  mulap0bad  8990  divadddivap  9060  recnz  9744  lbzbi  10026  xadd4d  10298  ixxss1  10317  ixxss2  10318  ixxss12  10319  iccss2  10357  iccssioo2  10359  iccssico2  10360  iccen  10420  elfzole1  10574  infssfzcldc  10680  infssfzledc  10681  ioom  10706  elicore  10712  flqle  10726  flapge  10731  flaplt  10733  flqltnz  10737  addmodlteq  10850  expclzap  11016  hashennnuni  11234  zfz1isolem1  11308  hashdmprop2dom  11312  swrdsbslen  11454  ccatswrd  11458  ccatpfx  11489  recl  11634  sq01  11676  cvg1nlemcau  11766  cvg1nlemres  11767  resqrtth  11813  fimaxre2  12010  climcl  12067  reccn2ap  12098  nnf1o  12162  summodclem3  12166  sumpr  12199  fsump1i  12219  fisumcom2  12224  fsum00  12248  fsumparts  12256  mertenslemi1  12321  prodmodclem3  12361  fprodcom2fi  12412  addsin  12528  subsin  12529  addcos  12532  subcos  12533  sinbnd2  12540  cosbnd2  12541  sin01gt0  12548  cos01gt0  12549  divgcdz  12767  divgcdnn  12771  gcdaddm  12780  bezoutlemstep  12793  dvdsgcdb  12809  dfgcd2  12810  mulgcd  12812  gcdzeq  12818  dvdsmulgcd  12821  sqgcd  12825  bezoutr  12828  lcmval  12860  lcmcllem  12864  gcddvdslcm  12870  lcmgcdlem  12874  lcmgcd  12875  lcmgcdeq  12880  lcmdvdsb  12881  mulgcddvds  12891  rpmulgcd2  12892  qredeu  12894  rpdvds  12896  isprm3  12915  divgcdodd  12941  coprm  12942  rpexp  12951  sqrt2irr  12960  qnumcl  12987  qnumdencoprm  12992  divnumden  12995  numsq  13002  phimullem  13026  eulerthlem1  13028  prmdiveq  13037  prmdivdiv  13038  hashgcdlem  13039  odzcl  13045  reumodprminv  13055  pythagtriplem19  13084  pclemub  13089  pcprendvds  13092  pcprendvds2  13093  pcpre1  13094  pcpremul  13095  pceulem  13096  pceu  13097  pczpre  13099  pczcl  13100  pcgcd1  13130  pc2dvds  13132  pcaddlem  13141  pcmpt  13145  pockthlem  13158  prmunb  13164  4sqlem7  13186  4sqlem8  13187  4sqlem9  13188  4sqlem10  13189  4sqlem14  13206  4sqlem15  13207  4sqlem16  13208  4sqlem17  13209  4sqlem18  13210  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemimin  13301  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsv  13305  ballotfilemsgt1  13306  ballotfilemsdom  13307  ballotfilemsel1i  13308  ballotfilemsf1o  13309  ballotfilemsi  13310  ballotfilemsima  13311  ballotfilemscr  13314  ballotfilemrv  13315  ballotfilemrv2  13317  ballotfilemro  13318  ballotfilemfrc  13322  ballotfilemfrci  13323  ballotfilemfrceq  13324  ballotfilemfrcn0  13325  ballotfilemrc  13326  ballotfilemirc  13327  ballotfilemrinv0  13328  ballotfilem1ri  13330  ennnfonelemg  13346  ennnfonelemf1  13361  ctiunctlemu1st  13377  nninfdclemf  13392  nninfdclemp1  13393  mgmidcl  13751  gzsumfzval  13764  gzsumval2  13767  mndlid  13801  imasmndf1  13814  dfgrp3mlem  13956  grplactf1o  13961  imasgrpf1  13968  subgsubm  14052  qusgrp  14088  ghmgrp1  14101  ghmf  14103  ghmnsgpreima  14125  kerf1ghm  14130  conjsubg  14133  resscntz  14160  gzsumsplit0  14232  gsumvalfi  14236  prdsmndd  14285  prdsgrpd  14288  prdsinvgd  14289  imasrng  14346  srgdilem  14364  srgdi  14369  srglidm  14374  ringdilem  14407  ringdi  14414  ringlidm  14419  imasring  14460  imasringf1  14461  dvdsrcld  14495  unitcld  14506  unitmulcl  14511  unitnegcl  14528  rhmghm  14560  elrhmunit  14575  subrgss  14621  subrgrcl  14625  rrgsupp  14665  lmodvscl  14732  lmodvsdi  14739  lmodvsdir  14740  lsslsp  14857  qusring  14955  crngridl  14958  znunit  15085  znrrg  15086  assaass  15095  assalmod  15097  psrbaglesuppg  15148  psrbagcon  15153  psrbagconcl  15155  psrelbas  15158  psraddcl  15163  rhmpsrfilem2  15164  psrmulfval  15166  psrlidmfi  15178  mplrcl  15184  uniopn  15201  restbasg  15368  cntop1  15401  cnf  15404  cnpf2  15407  lmtopcnp  15450  psmetdmdm  15524  psmetf  15525  psmet0  15527  xmetf  15550  metf  15551  blhalf  15608  xmetxpbl  15708  ioo2bl  15751  tgioo  15754  cncff  15777  rescncf  15781  cdivcncfap  15804  cnopnap  15811  divcncfap  15814  dedekindeulemeu  15822  dedekindicclemeu  15831  ivthinclemlm  15834  ivthinclemlopn  15836  ivthinclemuopn  15838  ivthinclemdisj  15840  ivthdec  15844  ivthreinc  15845  limcimolemlt  15864  limcimo  15865  limccnpcntop  15875  limccnp2lem  15876  limccnp2cntop  15877  limccoap  15878  eldvap  15882  dvbsssg  15886  dvfgg  15888  dvaddxxbr  15901  dvmulxxbr  15902  dvcoapbr  15907  dvcj  15909  dvfre  15910  dvrecap  15913  plyco  15959  plycj  15961  sin0pilem1  15982  sin0pilem2  15983  pilem3  15984  tanrpcl  16038  tangtx  16039  zprmlogbaplem2  16190  zprmlogbaplem3  16191  ppiqsval2  16215  chtqge0  16221  chtqwordi  16237  chtublem  16269  perfect  16275  bposlem1  16285  bposlem4  16288  bposlem5  16289  bposlem9  16293  lgsne0  16336  lgseisen  16372  lgsquad2lem2  16380  2sqlem8a  16420  2sqlem8  16421  structgrssvtx  16462  edguhgr  16557  umgrpredgv  16567  umgrnloop2  16571  umgr2edg  16627  subuhgr  16692  subumgr  16694  subusgr  16695  wlkpropg  16744  wlkv  16746  wlkvtxeledgg  16764  wlkvtxiedgg  16766  wlk1walkdom  16779  trlsv  16804  clwwlksswrd  16817  clwwlkclwwlkn  16829  eupthv  16866  eupthseg  16872  eupth2lem3lem3fi  16890  eupth2lem3lem4fi  16893  eupth2lemsfi  16898  eulerpathprum  16900  nninfalllem1  17230  iooref1o  17262  als1d  17313  rals1d  17315  alseu1d  17349  ralseu1d  17351