Theorem simp1 1023

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simpl1  1026  simpr1  1029  simp1i  1032  simp1d  1035  simp11  1053  simp21  1056  simp31  1059  syld3an3  1318  3ianorr  1345  intn3an1d  1392  stoic4a  1476  stoic4b  1477  rsp2e  2583  ifnetruedc  3649  issod  4416  elirr  4639  sotri2  5134  sotri3  5135  funtpg  5381  funimaexglem  5413  feq123  5474  ftpg  5838  fsnunf  5854  foco2  5894  fcofo  5925  f1oiso2  5968  riotass  6001  ovmpox  6150  ovmpoga  6151  caovimo  6216  ofeq  6238  ofrval  6246  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  frecsuclem  6572  frecrdg  6574  domssr  6951  mapxpen  7034  diffifi  7083  unsnfidcex  7112  unsnfidcel  7113  unfidisj  7114  undifdc  7116  ssfidc  7130  iunfidisj  7145  sbthlemi9  7164  elfir  7172  djuassen  7432  dftap2  7470  mulcanenq  7605  ltanqg  7620  addnnnq0  7669  distrlem4prl  7804  distrlem4pru  7805  distrprg  7808  aptipr  7861  addsrpr  7965  mulsrpr  7966  mulasssrg  7978  ltpsrprg  8023  axmulass  8093  axpre-ltadd  8106  mul31  8310  addsubass  8389  subcan2  8404  subsub2  8407  subsub4  8412  npncan3  8417  pnpcan  8418  pnncan  8420  subcan  8434  subdi  8564  ltadd1  8609  leadd1  8610  leadd2  8611  ltsubadd  8612  lesubadd  8614  ltaddsub  8616  leaddsub  8618  lesub1  8636  lesub2  8637  ltsub1  8638  ltsub2  8639  ltaddsublt  8751  gt0add  8753  apreap  8767  lemul1  8773  reapmul1lem  8774  reapmul1  8775  reapadd1  8776  remulext1  8779  remulext2  8780  apadd2  8789  mulext2  8793  mulap0r  8795  leltap  8805  ltap  8813  apsub1  8822  recexaplem2  8832  mulcanap  8845  mulcanap2  8846  divvalap  8854  divcanap2  8860  diveqap0  8862  divrecap  8868  divrecap2  8869  divdirap  8877  divcanap3  8878  div11ap  8880  muldivdirap  8887  divcanap5  8894  redivclap  8911  div2negap  8915  apmul1  8968  apmul2  8969  div2subap  9017  ltdiv1  9048  ltmuldiv  9054  lemuldiv  9061  lt2msq1  9065  ltdiv23  9072  lediv23  9073  squeeze0  9084  ofnegsub  9142  difgtsumgt  9549  gtndiv  9575  eluz2  9761  eluzsub  9786  peano2uz  9817  nn01to3  9851  divge1  9958  ledivge1le  9961  addlelt  10003  xaddass  10104  xleadd1  10110  xltadd1  10111  ixxssixx  10137  lbico1  10165  lbicc2  10219  icoshftf1o  10226  fzen  10278  fzrev3  10322  fzrevral2  10341  nelfzo  10387  elfzo0  10421  elfzo0z  10424  fzosplitprm1  10481  qbtwnre  10517  flqwordi  10549  flqword2  10550  adddivflid  10553  flltdivnn0lt  10565  modqcl  10589  mulqmod0  10593  modqmulnn  10605  modqabs2  10621  addmodid  10635  modifeq2int  10649  modqeqmodmin  10657  seqeq2  10714  seqeq3  10715  seq1g  10726  seqp1g  10729  exp3val  10804  expnegap0  10810  expgt1  10840  exprecap  10843  leexp2a  10855  expubnd  10859  sqdivap  10866  expnbnd  10926  mulsubdivbinom2ap  10974  bccmpl  11017  fihashss  11081  leisorel  11102  ccatass  11189  ccats1val2  11221  swrdval  11233  swrdval2  11236  swrdlen2  11247  swrdfv2  11248  pfxfv  11269  pfxn0  11273  pfxnd  11274  swrdswrd  11290  pfxswrd  11291  pfxpfx  11293  ccats1pfxeqbi  11327  s3cl  11371  s3fv0g  11376  s3fv1g  11377  s3fv2g  11378  shftfibg  11398  mulreap  11442  abssubne0  11669  maxleast  11791  lemininf  11812  ltmininf  11813  xrmaxltsup  11836  xrmaxaddlem  11838  xrmaxadd  11839  xrmineqinf  11847  xrltmininf  11848  xrminltinf  11850  xrminadd  11853  climuni  11871  reccn2ap  11891  isumz  11968  fsumsplitsnun  11998  geoisum1c  12099  prod1dc  12165  efltim  12277  dvdscmulr  12399  dvdsmulcr  12400  summodnegmod  12401  modmulconst  12402  dvdsmultr2  12412  dvdsexp  12440  mulmoddvds  12442  modremain  12508  divgcdz  12560  gcdaddm  12573  dvdsgcdb  12602  gcdass  12604  mulgcd  12605  gcddiv  12608  rplpwr  12616  uzwodc  12626  lcmdvdsb  12674  lcmass  12675  mulgcddvds  12684  qredeq  12686  qredeu  12687  rpmul  12688  divgcdcoprmex  12692  cncongr1  12693  rpexp  12743  rpexp12i  12745  odzcllem  12833  odzdvds  12836  odzphi  12837  pythagtriplem15  12869  pcpremul  12884  pcdiv  12893  pcqmul  12894  pcqdiv  12898  dvdsprmpweq  12926  sumhashdc  12938  pcfaclem  12940  qexpz  12943  ctinf  13069  setsvala  13131  ressressg  13176  ressabsg  13177  rngbaseg  13237  ptex  13365  issubmnd  13543  ress0g  13544  imasmnd2  13553  gsumfzz  13596  grpasscan2  13665  grpidrcan  13666  grpidlcan  13667  grpinvadd  13679  grpsubeq0  13687  grppncan  13692  dfgrp3m  13700  grpsubpropd2  13706  pwsinvg  13713  imasgrp2  13715  mhmmnd  13721  mulgnegneg  13746  mulgaddcomlem  13750  mulgaddcom  13751  mulginvcom  13752  mulgmodid  13766  issubg  13778  nsgconj  13811  nsgid  13820  quselbasg  13835  quseccl0g  13836  ghmnsgima  13873  cmn4  13910  ablinvadd  13915  ablsub4  13918  abladdsub4  13919  ablpncan2  13921  rngpropd  13987  imasrng  13988  issrg  13997  ringidss  14061  ringcom  14063  imasring  14096  unitmulcl  14146  unitmulclb  14147  dvrcl  14168  unitdvcl  14169  dvrcan1  14173  dvrcan3  14174  issubrng  14232  subrngpropd  14249  rrgeq0  14298  islmod  14324  lmodcom  14366  rmodislmodlem  14383  rmodislmod  14384  lss0cl  14402  lssvnegcl  14409  lssintclm  14417  lssincl  14418  lspss  14432  lspun  14435  lspsnvsi  14451  lsslsp  14462  rnglidlmmgm  14529  rnglidlmsgrp  14530  rnglidlrng  14531  qus2idrng  14558  qusmulrng  14565  2basgeng  14825  clsss  14861  ntrss  14862  ntrin  14867  neiss  14893  restco  14917  restabs  14918  lmconst  14959  psmetsym  15072  psmetge0  15074  xmetge0  15108  xmetsym  15111  xmetresbl  15183  mopni3  15227  bdxmet  15244  bdmopn  15247  txmetcnp  15261  dvfvalap  15424  dvid  15438  dvidre  15440  dvcnp2cntop  15442  elplyr  15483  ply1term  15486  ptolemy  15567  rpcxpadd  15648  rpmulcxp  15652  rpdivcxp  15654  cxpmul  15655  rpcxple2  15661  rpcxplt2  15662  cxpcom  15681  rplogbval  15688  rplogbcl  15689  rprelogbmulexp  15699  relogbexpap  15701  logbleb  15704  logblt  15705  rplogbcxp  15706  rpcxplogb  15707  sgmppw  15735  lgslem1  15748  lgsfcl2  15754  lgsneg  15772  lgsne0  15786  lgssq2  15789  lgsdirnn0  15795  gausslemma2dlem1a  15806  lgsquad  15828  2lgsoddprmlem2  15854  funvtxvalg  15906  funiedgvalg  15907  lpvtx  15949  upgrex  15973  subumgredg2en  16141  iedginwlk  16227  eulerpathprum  16350  gfsumsn  16737