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  7342  supsnti  7345  supisoti  7350  ctssdccl  7451  ctfoex  7458  fodjum  7486  en2eleq  7547  djuen  7567  pw1if  7584  dftap2  7617  2omotaplemst  7624  exmidapne  7626  ccfunen  7630  dfplpq2  7721  ltbtwnnqq  7782  enq0tr  7801  elnp1st2nd  7843  prcdnql  7851  prnminu  7856  prloc  7858  genpcdl  7886  addnqprulem  7895  addlocprlemlt  7898  addlocprlemgt  7901  addlocprlem  7902  addlocpr  7903  nqprxx  7913  ltnqex  7916  addnqprlemfl  7926  addnqprlemfu  7927  appdivnq  7930  prmuloclemcalc  7932  prmuloc  7933  mullocprlem  7937  mulnqprlemfl  7942  mulnqprlemfu  7943  ltprordil  7956  ltnqpri  7961  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  ltexpri  7980  lteupri  7984  ltaprlem  7985  recexprlemell  7989  recexprlemelu  7990  recexprlemloc  7998  recexprlempr  7999  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1u  8003  aptipr  8008  cauappcvgprlemm  8012  cauappcvgprlemlol  8014  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlem1  8026  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemlol  8037  caucvgprlemladdfu  8044  caucvgprprlemloccalc  8051  caucvgprprlemnkltj  8056  caucvgprprlemnbj  8060  caucvgprprlemml  8061  caucvgprprlemlol  8065  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  suplocexprlemss  8082  suplocexprlemru  8086  suplocexprlemlub  8091  ltsrprg  8114  caucvgsrlemasr  8157  suplocsrlemb  8173  suplocsrlem  8175  suplocsr  8176  axcaucvglemcau  8265  axpre-suploclemres  8268  negf1o  8709  apreap  8915  apreim  8931  msqge0  8944  mulge0  8947  apti  8950  apsscn  8975  mulap0bad  8987  divadddivap  9057  recnz  9739  lbzbi  10016  xadd4d  10287  ixxss1  10306  ixxss2  10307  ixxss12  10308  iccss2  10346  iccssioo2  10348  iccssico2  10349  iccen  10409  elfzole1  10563  infssfzcldc  10669  infssfzledc  10670  ioom  10695  elicore  10701  flqle  10713  flqltnz  10722  addmodlteq  10835  expclzap  11001  hashennnuni  11218  zfz1isolem1  11292  hashdmprop2dom  11296  swrdsbslen  11438  ccatswrd  11442  ccatpfx  11473  recl  11618  sq01  11660  cvg1nlemcau  11750  cvg1nlemres  11751  resqrtth  11797  fimaxre2  11993  climcl  12048  reccn2ap  12079  nnf1o  12143  summodclem3  12147  sumpr  12180  fsump1i  12200  fisumcom2  12205  fsum00  12229  fsumparts  12237  mertenslemi1  12302  prodmodclem3  12342  fprodcom2fi  12393  addsin  12509  subsin  12510  addcos  12513  subcos  12514  sinbnd2  12521  cosbnd2  12522  sin01gt0  12529  cos01gt0  12530  divgcdz  12748  divgcdnn  12752  gcdaddm  12761  bezoutlemstep  12774  dvdsgcdb  12790  dfgcd2  12791  mulgcd  12793  gcdzeq  12799  dvdsmulgcd  12802  sqgcd  12806  bezoutr  12809  lcmval  12841  lcmcllem  12845  gcddvdslcm  12851  lcmgcdlem  12855  lcmgcd  12856  lcmgcdeq  12861  lcmdvdsb  12862  mulgcddvds  12872  rpmulgcd2  12873  qredeu  12875  rpdvds  12877  isprm3  12896  divgcdodd  12921  coprm  12922  rpexp  12931  sqrt2irr  12940  qnumcl  12966  qnumdencoprm  12971  divnumden  12974  numsq  12981  phimullem  13003  eulerthlem1  13005  prmdiveq  13014  prmdivdiv  13015  hashgcdlem  13016  odzcl  13022  reumodprminv  13032  pythagtriplem19  13061  pclemub  13066  pcprendvds  13069  pcprendvds2  13070  pcpre1  13071  pcpremul  13072  pceulem  13073  pceu  13074  pczpre  13076  pczcl  13077  pcgcd1  13107  pc2dvds  13109  pcaddlem  13118  pcmpt  13122  pockthlem  13135  prmunb  13141  4sqlem7  13163  4sqlem8  13164  4sqlem9  13165  4sqlem10  13166  4sqlem14  13183  4sqlem15  13184  4sqlem16  13185  4sqlem17  13186  4sqlem18  13187  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilem4  13241  ballotfilemi1  13245  ballotfilemimin  13249  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemsv  13253  ballotfilemsgt1  13254  ballotfilemsdom  13255  ballotfilemsel1i  13256  ballotfilemsf1o  13257  ballotfilemsi  13258  ballotfilemsima  13259  ballotfilemscr  13262  ballotfilemrv  13263  ballotfilemrv2  13265  ballotfilemro  13266  ballotfilemfrc  13270  ballotfilemfrci  13271  ballotfilemfrceq  13272  ballotfilemfrcn0  13273  ballotfilemrc  13274  ballotfilemirc  13275  ballotfilemrinv0  13276  ballotfilem1ri  13278  ennnfonelemg  13294  ennnfonelemf1  13309  ctiunctlemu1st  13325  nninfdclemf  13340  nninfdclemp1  13341  mgmidcl  13698  gzsumfzval  13711  gzsumval2  13714  mndlid  13748  imasmndf1  13761  dfgrp3mlem  13903  grplactf1o  13908  imasgrpf1  13915  subgsubm  13999  qusgrp  14035  ghmgrp1  14048  ghmf  14050  ghmnsgpreima  14072  kerf1ghm  14077  conjsubg  14080  gzsumsplit0  14148  gsumvalfi  14152  prdsmndd  14194  prdsgrpd  14197  prdsinvgd  14198  imasrng  14255  srgdilem  14273  srgdi  14278  srglidm  14283  ringdilem  14316  ringdi  14323  ringlidm  14328  imasring  14369  imasringf1  14370  dvdsrcld  14404  unitcld  14415  unitmulcl  14420  unitnegcl  14437  rhmghm  14469  elrhmunit  14484  subrgss  14530  subrgrcl  14534  rrgsupp  14574  lmodvscl  14641  lmodvsdi  14648  lmodvsdir  14649  lsslsp  14766  qusring  14864  crngridl  14867  znunit  14994  znrrg  14995  assaass  15004  assalmod  15006  psrbaglesuppg  15057  psrbagcon  15062  psrbagconcl  15063  psrelbas  15066  psraddcl  15071  mplrcl  15085  uniopn  15102  restbasg  15269  cntop1  15302  cnf  15305  cnpf2  15308  lmtopcnp  15351  psmetdmdm  15425  psmetf  15426  psmet0  15428  xmetf  15451  metf  15452  blhalf  15509  xmetxpbl  15609  ioo2bl  15652  tgioo  15655  cncff  15678  rescncf  15682  cdivcncfap  15705  cnopnap  15712  divcncfap  15715  dedekindeulemeu  15723  dedekindicclemeu  15732  ivthinclemlm  15735  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthinclemdisj  15741  ivthdec  15745  ivthreinc  15746  limcimolemlt  15765  limcimo  15766  limccnpcntop  15776  limccnp2lem  15777  limccnp2cntop  15778  limccoap  15779  eldvap  15783  dvbsssg  15787  dvfgg  15789  dvaddxxbr  15802  dvmulxxbr  15803  dvcoapbr  15808  dvcj  15810  dvfre  15811  dvrecap  15814  plyco  15860  plycj  15862  sin0pilem1  15882  sin0pilem2  15883  pilem3  15884  tanrpcl  15938  tangtx  15939  perfect  16115  lgsne0  16157  lgseisen  16193  lgsquad2lem2  16201  2sqlem8a  16241  2sqlem8  16242  structgrssvtx  16283  edguhgr  16378  umgrpredgv  16388  umgrnloop2  16392  umgr2edg  16448  subuhgr  16513  subumgr  16515  subusgr  16516  wlkpropg  16565  wlkv  16567  wlkvtxeledgg  16585  wlkvtxiedgg  16587  wlk1walkdom  16600  trlsv  16625  clwwlksswrd  16638  clwwlkclwwlkn  16650  eupthv  16687  eupthseg  16693  eupth2lem3lem3fi  16711  eupth2lem3lem4fi  16714  eupth2lemsfi  16719  eulerpathprum  16721  nninfalllem1  17051  iooref1o  17083  als1d  17133  rals1d  17135  alseu1d  17169  ralseu1d  17171