Theorem simp1 1028

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

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

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl1  1031  simpr1  1034  simp1i  1037  simp1d  1040  simp11  1058  simp21  1061  simp31  1064  syld3an3  1323  3ianorr  1350  intn3an1d  1397  stoic4a  1481  stoic4b  1482  rsp2e  2601  ifnetruedc  3684  issod  4464  elirr  4688  sotri2  5185  sotri3  5186  funtpg  5432  funimaexglem  5464  feq123  5525  ftpg  5899  fsnunf  5915  foco2  5959  fcofo  5990  f1oiso2  6033  riotass  6068  ovmpox  6217  ovmpoga  6218  caovimo  6283  ofeq  6305  ofrval  6313  fvn0elsuppb  6492  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  frecsuclem  6677  frecrdg  6679  domssr  7064  mapxpen  7148  diffifi  7198  unsnfidcex  7227  unsnfidcel  7228  unfidisj  7229  undifdc  7231  ssfidc  7245  iunfidisj  7260  fissfi  7263  sbthlemi9  7282  elfir  7307  fdcf1  7316  djuassen  7573  dftap2  7617  mulcanenq  7752  ltanqg  7767  addnnnq0  7816  distrlem4prl  7951  distrlem4pru  7952  distrprg  7955  aptipr  8008  addsrpr  8112  mulsrpr  8113  mulasssrg  8125  ltpsrprg  8170  axmulass  8240  axpre-ltadd  8253  mul31  8457  addsubass  8536  subcan2  8551  subsub2  8554  subsub4  8559  npncan3  8564  pnpcan  8565  pnncan  8567  subcan  8581  subdi  8712  ltadd1  8757  leadd1  8758  leadd2  8759  ltsubadd  8760  lesubadd  8762  ltaddsub  8764  leaddsub  8766  lesub1  8784  lesub2  8785  ltsub1  8786  ltsub2  8787  ltaddsublt  8899  gt0add  8901  apreap  8915  lemul1  8921  reapmul1lem  8922  reapmul1  8923  reapadd1  8924  remulext1  8927  remulext2  8928  apadd2  8937  mulext2  8941  mulap0r  8943  leltap  8953  ltap  8961  apsub1  8970  recexaplem2  8980  mulcanap  8993  mulcanap2  8994  divvalap  9004  divcanap2  9010  diveqap0  9012  divrecap  9018  divrecap2  9019  divdirap  9027  divcanap3  9028  div11ap  9030  muldivdirap  9037  divcanap5  9044  redivclap  9061  div2negap  9065  apmul1  9118  apmul2  9119  div2subap  9167  ltdiv1  9198  ltmuldiv  9204  lemuldiv  9211  lt2msq1  9215  ltdiv23  9222  lediv23  9223  squeeze0  9234  ofnegsub  9292  difgtsumgt  9714  zfidc  9723  gtndiv  9741  eluz2  9927  eluzsub  9952  peano2uz  9983  nn01to3  10017  divge1  10124  ledivge1le  10127  addlelt  10169  xaddass  10271  xleadd1  10277  xltadd1  10278  ixxssixx  10304  lbico1  10332  lbicc2  10386  icoshftf1o  10393  fzen  10447  fzrev3  10494  fzrevral2  10513  nelfzo  10559  elfzo0  10593  elfzo0z  10596  fzosplitprm1  10653  qbtwnre  10691  flqwordi  10723  flqword2  10724  adddivflid  10727  flltdivnn0lt  10739  modqcl  10763  mulqmod0  10767  modqmulnn  10779  modqabs2  10795  addmodid  10809  modifeq2int  10823  modqeqmodmin  10831  seqeq2  10888  seqeq3  10889  seq1g  10900  seqp1g  10903  exp3val  10978  expnegap0  10984  expgt1  11014  exprecap  11017  leexp2a  11029  expubnd  11033  sqdivap  11040  expnbnd  11101  mulsubdivbinom2ap  11149  bccmpl  11192  fihashss  11257  leisorel  11289  ccatass  11376  ccats1val2  11408  swrdval  11420  swrdval2  11423  swrdlen2  11434  swrdfv2  11435  pfxfv  11456  pfxn0  11460  pfxnd  11461  swrdswrd  11477  pfxswrd  11478  pfxpfx  11480  ccats1pfxeqbi  11514  s3cl  11558  s3fv0g  11563  s3fv1g  11564  s3fv2g  11565  shftfibg  11585  mulreap  11629  abssubne0  11857  maxleast  11979  lemininf  12000  ltmininf  12001  xrmaxltsup  12024  xrmaxaddlem  12026  xrmaxadd  12027  xrmineqinf  12035  xrltmininf  12036  xrminltinf  12038  xrminadd  12041  climuni  12059  reccn2ap  12079  isumz  12156  fsumsplitsnun  12186  geoisum1c  12287  prod1dc  12353  efltim  12465  dvdscmulr  12587  dvdsmulcr  12588  summodnegmod  12589  modmulconst  12590  dvdsmultr2  12600  dvdsexp  12628  mulmoddvds  12630  modremain  12696  divgcdz  12748  gcdaddm  12761  dvdsgcdb  12790  gcdass  12792  mulgcd  12793  gcddiv  12796  rplpwr  12804  uzwodc  12814  lcmdvdsb  12862  lcmass  12863  mulgcddvds  12872  qredeq  12874  qredeu  12875  rpmul  12876  divgcdcoprmex  12880  cncongr1  12881  rpexp  12931  rpexp12i  12933  odzcllem  13021  odzdvds  13024  odzphi  13025  pythagtriplem15  13057  pcpremul  13072  pcdiv  13081  pcqmul  13082  pcqdiv  13086  dvdsprmpweq  13114  sumhashdc  13126  pcfaclem  13128  qexpz  13131  ballotfilemfrcn0  13273  ctinf  13321  setsvala  13383  ressressg  13429  ressabsg  13430  rngbaseg  13490  ptex  13618  issubmnd  13755  ress0g  13756  imasmnd2  13759  grpasscan2  13869  grpidrcan  13870  grpidlcan  13871  grpinvadd  13883  grpsubeq0  13891  grppncan  13896  dfgrp3m  13904  grpsubpropd2  13910  imasgrp2  13913  mhmmnd  13919  mulgnegneg  13944  mulgaddcomlem  13948  mulgaddcom  13949  mulginvcom  13950  mulgmodid  13964  issubg  13976  nsgconj  14009  nsgid  14018  quselbasg  14033  quseccl0g  14034  ghmnsgima  14071  cmn4  14108  ablinvadd  14114  ablsub4  14117  abladdsub4  14118  ablpncan2  14120  gsumsncmn  14156  gsumconstcmn  14166  pwsinvg  14215  rngpropd  14254  imasrng  14255  issrg  14269  ringidss  14334  ringcom  14336  imasring  14369  unitmulcl  14420  unitmulclb  14421  dvrcl  14442  unitdvcl  14443  dvrcan1  14447  dvrcan3  14448  issubrng  14507  subrngpropd  14524  rrgeq0  14573  islmod  14627  lmodcom  14670  rmodislmodlem  14687  rmodislmod  14688  lss0cl  14706  lssvnegcl  14713  lssintclm  14721  lssincl  14722  lspss  14736  lspun  14739  lspsnvsi  14755  lsslsp  14766  rnglidlmmgm  14833  rnglidlmsgrp  14834  rnglidlrng  14835  qus2idrng  14862  qusmulrng  14869  assa2ass  15009  assa2ass2  15010  aspid  15017  aspss  15019  asclmul1  15029  asclmul2  15030  asclinvg  15032  psrbaglecl  15060  psrbagcon  15062  2basgeng  15183  clsss  15219  ntrss  15220  ntrin  15225  neiss  15251  restco  15275  restabs  15276  lmconst  15317  psmetsym  15430  psmetge0  15432  xmetge0  15466  xmetsym  15469  xmetresbl  15541  mopni3  15585  bdxmet  15602  bdmopn  15605  txmetcnp  15619  dvfvalap  15782  dvid  15796  dvidre  15798  dvcnp2cntop  15800  elplyr  15841  ply1term  15844  ptolemy  15925  logfac  15995  rpcxpadd  16007  rpmulcxp  16011  rpdivcxp  16013  cxpmul  16014  rpcxple2  16020  rpcxplt2  16021  cxpcom  16040  rplogbval  16047  rplogbcl  16048  rprelogbmulexp  16058  relogbexpap  16060  logbleb  16063  logblt  16064  rplogbcxp  16065  rpcxplogb  16066  sgmppw  16106  lgslem1  16119  lgsfcl2  16125  lgsneg  16143  lgsne0  16157  lgssq2  16160  lgsdirnn0  16166  gausslemma2dlem1a  16177  lgsquad  16199  2lgsoddprmlem2  16225  funvtxvalg  16277  funiedgvalg  16278  lpvtx  16320  upgrex  16344  subumgredg2en  16512  iedginwlk  16598  eulerpathprum  16721  dichmul0or  16760