Theorem simp1 1021

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simpl1  1024  simpr1  1027  simp1i  1030  simp1d  1033  simp11  1051  simp21  1054  simp31  1057  syld3an3  1316  3ianorr  1343  intn3an1d  1390  stoic4a  1474  stoic4b  1475  rsp2e  2581  ifnetruedc  3647  issod  4414  elirr  4637  sotri2  5132  sotri3  5133  funtpg  5378  funimaexglem  5410  feq123  5471  ftpg  5833  fsnunf  5849  foco2  5889  fcofo  5920  f1oiso2  5963  riotass  5996  ovmpox  6145  ovmpoga  6146  caovimo  6211  ofeq  6233  ofrval  6241  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  frecsuclem  6567  frecrdg  6569  domssr  6946  mapxpen  7029  diffifi  7076  unsnfidcex  7105  unsnfidcel  7106  unfidisj  7107  undifdc  7109  ssfidc  7122  iunfidisj  7136  sbthlemi9  7155  elfir  7163  djuassen  7422  dftap2  7460  mulcanenq  7595  ltanqg  7610  addnnnq0  7659  distrlem4prl  7794  distrlem4pru  7795  distrprg  7798  aptipr  7851  addsrpr  7955  mulsrpr  7956  mulasssrg  7968  ltpsrprg  8013  axmulass  8083  axpre-ltadd  8096  mul31  8300  addsubass  8379  subcan2  8394  subsub2  8397  subsub4  8402  npncan3  8407  pnpcan  8408  pnncan  8410  subcan  8424  subdi  8554  ltadd1  8599  leadd1  8600  leadd2  8601  ltsubadd  8602  lesubadd  8604  ltaddsub  8606  leaddsub  8608  lesub1  8626  lesub2  8627  ltsub1  8628  ltsub2  8629  ltaddsublt  8741  gt0add  8743  apreap  8757  lemul1  8763  reapmul1lem  8764  reapmul1  8765  reapadd1  8766  remulext1  8769  remulext2  8770  apadd2  8779  mulext2  8783  mulap0r  8785  leltap  8795  ltap  8803  apsub1  8812  recexaplem2  8822  mulcanap  8835  mulcanap2  8836  divvalap  8844  divcanap2  8850  diveqap0  8852  divrecap  8858  divrecap2  8859  divdirap  8867  divcanap3  8868  div11ap  8870  muldivdirap  8877  divcanap5  8884  redivclap  8901  div2negap  8905  apmul1  8958  apmul2  8959  div2subap  9007  ltdiv1  9038  ltmuldiv  9044  lemuldiv  9051  lt2msq1  9055  ltdiv23  9062  lediv23  9063  squeeze0  9074  ofnegsub  9132  difgtsumgt  9539  gtndiv  9565  eluz2  9751  eluzsub  9776  peano2uz  9807  nn01to3  9841  divge1  9948  ledivge1le  9951  addlelt  9993  xaddass  10094  xleadd1  10100  xltadd1  10101  ixxssixx  10127  lbico1  10155  lbicc2  10209  icoshftf1o  10216  fzen  10268  fzrev3  10312  fzrevral2  10331  nelfzo  10377  elfzo0  10411  elfzo0z  10413  fzosplitprm1  10470  qbtwnre  10506  flqwordi  10538  flqword2  10539  adddivflid  10542  flltdivnn0lt  10554  modqcl  10578  mulqmod0  10582  modqmulnn  10594  modqabs2  10610  addmodid  10624  modifeq2int  10638  modqeqmodmin  10646  seqeq2  10703  seqeq3  10704  seq1g  10715  seqp1g  10718  exp3val  10793  expnegap0  10799  expgt1  10829  exprecap  10832  leexp2a  10844  expubnd  10848  sqdivap  10855  expnbnd  10915  mulsubdivbinom2ap  10963  bccmpl  11006  fihashss  11070  leisorel  11091  ccatass  11175  ccats1val2  11207  swrdval  11219  swrdval2  11222  swrdlen2  11233  swrdfv2  11234  pfxfv  11255  pfxn0  11259  pfxnd  11260  swrdswrd  11276  pfxswrd  11277  pfxpfx  11279  ccats1pfxeqbi  11313  s3cl  11357  s3fv0g  11362  s3fv1g  11363  s3fv2g  11364  shftfibg  11371  mulreap  11415  abssubne0  11642  maxleast  11764  lemininf  11785  ltmininf  11786  xrmaxltsup  11809  xrmaxaddlem  11811  xrmaxadd  11812  xrmineqinf  11820  xrltmininf  11821  xrminltinf  11823  xrminadd  11826  climuni  11844  reccn2ap  11864  isumz  11940  fsumsplitsnun  11970  geoisum1c  12071  prod1dc  12137  efltim  12249  dvdscmulr  12371  dvdsmulcr  12372  summodnegmod  12373  modmulconst  12374  dvdsmultr2  12384  dvdsexp  12412  mulmoddvds  12414  modremain  12480  divgcdz  12532  gcdaddm  12545  dvdsgcdb  12574  gcdass  12576  mulgcd  12577  gcddiv  12580  rplpwr  12588  uzwodc  12598  lcmdvdsb  12646  lcmass  12647  mulgcddvds  12656  qredeq  12658  qredeu  12659  rpmul  12660  divgcdcoprmex  12664  cncongr1  12665  rpexp  12715  rpexp12i  12717  odzcllem  12805  odzdvds  12808  odzphi  12809  pythagtriplem15  12841  pcpremul  12856  pcdiv  12865  pcqmul  12866  pcqdiv  12870  dvdsprmpweq  12898  sumhashdc  12910  pcfaclem  12912  qexpz  12915  ctinf  13041  setsvala  13103  ressressg  13148  ressabsg  13149  rngbaseg  13209  ptex  13337  issubmnd  13515  ress0g  13516  imasmnd2  13525  gsumfzz  13568  grpasscan2  13637  grpidrcan  13638  grpidlcan  13639  grpinvadd  13651  grpsubeq0  13659  grppncan  13664  dfgrp3m  13672  grpsubpropd2  13678  pwsinvg  13685  imasgrp2  13687  mhmmnd  13693  mulgnegneg  13718  mulgaddcomlem  13722  mulgaddcom  13723  mulginvcom  13724  mulgmodid  13738  issubg  13750  nsgconj  13783  nsgid  13792  quselbasg  13807  quseccl0g  13808  ghmnsgima  13845  cmn4  13882  ablinvadd  13887  ablsub4  13890  abladdsub4  13891  ablpncan2  13893  rngpropd  13958  imasrng  13959  issrg  13968  ringidss  14032  ringcom  14034  imasring  14067  unitmulcl  14117  unitmulclb  14118  dvrcl  14139  unitdvcl  14140  dvrcan1  14144  dvrcan3  14145  issubrng  14203  subrngpropd  14220  rrgeq0  14269  islmod  14295  lmodcom  14337  rmodislmodlem  14354  rmodislmod  14355  lss0cl  14373  lssvnegcl  14380  lssintclm  14388  lssincl  14389  lspss  14403  lspun  14406  lspsnvsi  14422  lsslsp  14433  rnglidlmmgm  14500  rnglidlmsgrp  14501  rnglidlrng  14502  qus2idrng  14529  qusmulrng  14536  2basgeng  14796  clsss  14832  ntrss  14833  ntrin  14838  neiss  14864  restco  14888  restabs  14889  lmconst  14930  psmetsym  15043  psmetge0  15045  xmetge0  15079  xmetsym  15082  xmetresbl  15154  mopni3  15198  bdxmet  15215  bdmopn  15218  txmetcnp  15232  dvfvalap  15395  dvid  15409  dvidre  15411  dvcnp2cntop  15413  elplyr  15454  ply1term  15457  ptolemy  15538  rpcxpadd  15619  rpmulcxp  15623  rpdivcxp  15625  cxpmul  15626  rpcxple2  15632  rpcxplt2  15633  cxpcom  15652  rplogbval  15659  rplogbcl  15660  rprelogbmulexp  15670  relogbexpap  15672  logbleb  15675  logblt  15676  rplogbcxp  15677  rpcxplogb  15678  sgmppw  15706  lgslem1  15719  lgsfcl2  15725  lgsneg  15743  lgsne0  15757  lgssq2  15760  lgsdirnn0  15766  gausslemma2dlem1a  15777  lgsquad  15799  2lgsoddprmlem2  15825  funvtxvalg  15877  funiedgvalg  15878  lpvtx  15920  upgrex  15944  iedginwlk  16154