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  5837  fsnunf  5853  foco2  5893  fcofo  5924  f1oiso2  5967  riotass  6000  ovmpox  6149  ovmpoga  6150  caovimo  6215  ofeq  6237  ofrval  6245  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  frecsuclem  6571  frecrdg  6573  domssr  6950  mapxpen  7033  diffifi  7082  unsnfidcex  7111  unsnfidcel  7112  unfidisj  7113  undifdc  7115  ssfidc  7129  iunfidisj  7144  sbthlemi9  7163  elfir  7171  djuassen  7431  dftap2  7469  mulcanenq  7604  ltanqg  7619  addnnnq0  7668  distrlem4prl  7803  distrlem4pru  7804  distrprg  7807  aptipr  7860  addsrpr  7964  mulsrpr  7965  mulasssrg  7977  ltpsrprg  8022  axmulass  8092  axpre-ltadd  8105  mul31  8309  addsubass  8388  subcan2  8403  subsub2  8406  subsub4  8411  npncan3  8416  pnpcan  8417  pnncan  8419  subcan  8433  subdi  8563  ltadd1  8608  leadd1  8609  leadd2  8610  ltsubadd  8611  lesubadd  8613  ltaddsub  8615  leaddsub  8617  lesub1  8635  lesub2  8636  ltsub1  8637  ltsub2  8638  ltaddsublt  8750  gt0add  8752  apreap  8766  lemul1  8772  reapmul1lem  8773  reapmul1  8774  reapadd1  8775  remulext1  8778  remulext2  8779  apadd2  8788  mulext2  8792  mulap0r  8794  leltap  8804  ltap  8812  apsub1  8821  recexaplem2  8831  mulcanap  8844  mulcanap2  8845  divvalap  8853  divcanap2  8859  diveqap0  8861  divrecap  8867  divrecap2  8868  divdirap  8876  divcanap3  8877  div11ap  8879  muldivdirap  8886  divcanap5  8893  redivclap  8910  div2negap  8914  apmul1  8967  apmul2  8968  div2subap  9016  ltdiv1  9047  ltmuldiv  9053  lemuldiv  9060  lt2msq1  9064  ltdiv23  9071  lediv23  9072  squeeze0  9083  ofnegsub  9141  difgtsumgt  9548  gtndiv  9574  eluz2  9760  eluzsub  9785  peano2uz  9816  nn01to3  9850  divge1  9957  ledivge1le  9960  addlelt  10002  xaddass  10103  xleadd1  10109  xltadd1  10110  ixxssixx  10136  lbico1  10164  lbicc2  10218  icoshftf1o  10225  fzen  10277  fzrev3  10321  fzrevral2  10340  nelfzo  10386  elfzo0  10420  elfzo0z  10422  fzosplitprm1  10479  qbtwnre  10515  flqwordi  10547  flqword2  10548  adddivflid  10551  flltdivnn0lt  10563  modqcl  10587  mulqmod0  10591  modqmulnn  10603  modqabs2  10619  addmodid  10633  modifeq2int  10647  modqeqmodmin  10655  seqeq2  10712  seqeq3  10713  seq1g  10724  seqp1g  10727  exp3val  10802  expnegap0  10808  expgt1  10838  exprecap  10841  leexp2a  10853  expubnd  10857  sqdivap  10864  expnbnd  10924  mulsubdivbinom2ap  10972  bccmpl  11015  fihashss  11079  leisorel  11100  ccatass  11184  ccats1val2  11216  swrdval  11228  swrdval2  11231  swrdlen2  11242  swrdfv2  11243  pfxfv  11264  pfxn0  11268  pfxnd  11269  swrdswrd  11285  pfxswrd  11286  pfxpfx  11288  ccats1pfxeqbi  11322  s3cl  11366  s3fv0g  11371  s3fv1g  11372  s3fv2g  11373  shftfibg  11380  mulreap  11424  abssubne0  11651  maxleast  11773  lemininf  11794  ltmininf  11795  xrmaxltsup  11818  xrmaxaddlem  11820  xrmaxadd  11821  xrmineqinf  11829  xrltmininf  11830  xrminltinf  11832  xrminadd  11835  climuni  11853  reccn2ap  11873  isumz  11949  fsumsplitsnun  11979  geoisum1c  12080  prod1dc  12146  efltim  12258  dvdscmulr  12380  dvdsmulcr  12381  summodnegmod  12382  modmulconst  12383  dvdsmultr2  12393  dvdsexp  12421  mulmoddvds  12423  modremain  12489  divgcdz  12541  gcdaddm  12554  dvdsgcdb  12583  gcdass  12585  mulgcd  12586  gcddiv  12589  rplpwr  12597  uzwodc  12607  lcmdvdsb  12655  lcmass  12656  mulgcddvds  12665  qredeq  12667  qredeu  12668  rpmul  12669  divgcdcoprmex  12673  cncongr1  12674  rpexp  12724  rpexp12i  12726  odzcllem  12814  odzdvds  12817  odzphi  12818  pythagtriplem15  12850  pcpremul  12865  pcdiv  12874  pcqmul  12875  pcqdiv  12879  dvdsprmpweq  12907  sumhashdc  12919  pcfaclem  12921  qexpz  12924  ctinf  13050  setsvala  13112  ressressg  13157  ressabsg  13158  rngbaseg  13218  ptex  13346  issubmnd  13524  ress0g  13525  imasmnd2  13534  gsumfzz  13577  grpasscan2  13646  grpidrcan  13647  grpidlcan  13648  grpinvadd  13660  grpsubeq0  13668  grppncan  13673  dfgrp3m  13681  grpsubpropd2  13687  pwsinvg  13694  imasgrp2  13696  mhmmnd  13702  mulgnegneg  13727  mulgaddcomlem  13731  mulgaddcom  13732  mulginvcom  13733  mulgmodid  13747  issubg  13759  nsgconj  13792  nsgid  13801  quselbasg  13816  quseccl0g  13817  ghmnsgima  13854  cmn4  13891  ablinvadd  13896  ablsub4  13899  abladdsub4  13900  ablpncan2  13902  rngpropd  13967  imasrng  13968  issrg  13977  ringidss  14041  ringcom  14043  imasring  14076  unitmulcl  14126  unitmulclb  14127  dvrcl  14148  unitdvcl  14149  dvrcan1  14153  dvrcan3  14154  issubrng  14212  subrngpropd  14229  rrgeq0  14278  islmod  14304  lmodcom  14346  rmodislmodlem  14363  rmodislmod  14364  lss0cl  14382  lssvnegcl  14389  lssintclm  14397  lssincl  14398  lspss  14412  lspun  14415  lspsnvsi  14431  lsslsp  14442  rnglidlmmgm  14509  rnglidlmsgrp  14510  rnglidlrng  14511  qus2idrng  14538  qusmulrng  14545  2basgeng  14805  clsss  14841  ntrss  14842  ntrin  14847  neiss  14873  restco  14897  restabs  14898  lmconst  14939  psmetsym  15052  psmetge0  15054  xmetge0  15088  xmetsym  15091  xmetresbl  15163  mopni3  15207  bdxmet  15224  bdmopn  15227  txmetcnp  15241  dvfvalap  15404  dvid  15418  dvidre  15420  dvcnp2cntop  15422  elplyr  15463  ply1term  15466  ptolemy  15547  rpcxpadd  15628  rpmulcxp  15632  rpdivcxp  15634  cxpmul  15635  rpcxple2  15641  rpcxplt2  15642  cxpcom  15661  rplogbval  15668  rplogbcl  15669  rprelogbmulexp  15679  relogbexpap  15681  logbleb  15684  logblt  15685  rplogbcxp  15686  rpcxplogb  15687  sgmppw  15715  lgslem1  15728  lgsfcl2  15734  lgsneg  15752  lgsne0  15766  lgssq2  15769  lgsdirnn0  15775  gausslemma2dlem1a  15786  lgsquad  15808  2lgsoddprmlem2  15834  funvtxvalg  15886  funiedgvalg  15887  lpvtx  15929  upgrex  15953  subumgredg2en  16121  iedginwlk  16207