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  4466  elirr  4690  sotri2  5188  sotri3  5189  funtpg  5435  funimaexglem  5467  feq123  5528  ftpg  5902  fsnunf  5918  foco2  5962  fcofo  5993  f1oiso2  6036  riotass  6071  ovmpox  6220  ovmpoga  6221  caovimo  6286  ofeq  6308  ofrval  6317  fvn0elsuppb  6496  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  frecsuclem  6681  frecrdg  6683  domssr  7068  mapxpen  7152  diffifi  7202  unsnfidcex  7231  unsnfidcel  7232  unfidisj  7233  undifdc  7235  ssfidc  7249  iunfidisj  7264  fissfi  7267  sbthlemi9  7287  elfir  7312  fdcf1  7321  djuassen  7579  dftap2  7623  mulcanenq  7758  ltanqg  7773  addnnnq0  7822  distrlem4prl  7957  distrlem4pru  7958  distrprg  7961  aptipr  8014  addsrpr  8118  mulsrpr  8119  mulasssrg  8131  ltpsrprg  8176  axmulass  8246  axpre-ltadd  8259  mul31  8464  addsubass  8543  subcan2  8558  subsub2  8561  subsub4  8566  npncan3  8571  pnpcan  8572  pnncan  8574  subcan  8588  subdi  8719  ltadd1  8764  leadd1  8765  leadd2  8766  ltsubadd  8767  lesubadd  8769  ltaddsub  8771  leaddsub  8773  lesub1  8791  lesub2  8792  ltsub1  8793  ltsub2  8794  ltaddsublt  8907  gt0add  8909  apreap  8923  lemul1  8929  reapmul1lem  8930  reapmul1  8931  reapadd1  8932  remulext1  8935  remulext2  8936  apadd2  8945  mulext2  8949  mulap0r  8951  leltap  8961  ltap  8969  apsub1  8978  recexaplem2  8988  mulcanap  9001  mulcanap2  9002  divvalap  9012  divcanap2  9018  diveqap0  9020  divrecap  9026  divrecap2  9027  divdirap  9035  divcanap3  9036  div11ap  9038  muldivdirap  9045  divcanap5  9052  redivclap  9069  div2negap  9073  apmul1  9126  apmul2  9127  div2subap  9175  ltdiv1  9206  ltmuldiv  9212  lemuldiv  9219  lt2msq1  9223  ltdiv23  9230  lediv23  9231  squeeze0  9242  ofsubeq0  9300  ofnegsub  9301  difgtsumgt  9725  zfidc  9734  gtndiv  9752  eluz2  9943  eluzsub  9968  peano2uz  9999  nn01to3  10033  divge1  10141  ledivge1le  10144  addlelt  10186  xaddass  10288  xleadd1  10294  xltadd1  10295  ixxssixx  10321  lbico1  10349  lbicc2  10403  icoshftf1o  10410  fzen  10464  fzrev3  10511  fzrevral2  10530  nelfzo  10576  elfzo0  10610  elfzo0z  10613  fzosplitprm1  10670  qbtwnre  10708  flqwordi  10744  flqword2  10745  adddivflid  10748  flltdivnn0lt  10760  modqcl  10784  mulqmod0  10788  modqmulnn  10800  modqabs2  10816  addmodid  10830  modifeq2int  10844  modqeqmodmin  10852  seqeq2  10909  seqeq3  10910  seq1g  10921  seqp1g  10924  exp3val  10999  expnegap0  11005  expgt1  11035  exprecap  11038  leexp2a  11050  expubnd  11054  sqdivap  11061  expnbnd  11122  mulsubdivbinom2ap  11171  bccmpl  11214  fihashss  11279  leisorel  11311  ccatass  11398  ccats1val2  11430  swrdval  11442  swrdval2  11445  swrdlen2  11456  swrdfv2  11457  pfxfv  11478  pfxn0  11482  pfxnd  11483  swrdswrd  11499  pfxswrd  11500  pfxpfx  11502  ccats1pfxeqbi  11536  s3cl  11580  s3fv0g  11585  s3fv1g  11586  s3fv2g  11587  shftfibg  11607  mulreap  11651  abssubne0  11880  maxleast  12002  lemininf  12024  ltmininf  12025  xrmaxltsup  12049  xrmaxaddlem  12051  xrmaxadd  12052  xrmineqinf  12060  xrltmininf  12061  xrminltinf  12063  xrminadd  12066  climuni  12084  reccn2ap  12104  isumz  12181  fsumsplitsnun  12211  geoisum1c  12312  prod1dc  12378  efltim  12490  dvdscmulr  12612  dvdsmulcr  12613  summodnegmod  12614  modmulconst  12615  dvdsmultr2  12625  dvdsexp  12653  mulmoddvds  12655  modremain  12721  divgcdz  12773  gcdaddm  12786  dvdsgcdb  12815  gcdass  12817  mulgcd  12818  gcddiv  12821  rplpwr  12829  uzwodc  12839  lcmdvdsb  12887  lcmass  12888  mulgcddvds  12897  qredeq  12899  qredeu  12900  rpmul  12901  divgcdcoprmex  12905  cncongr1  12906  rpexp  12957  rpexp12i  12959  odzcllem  13050  odzdvds  13053  odzphi  13054  pythagtriplem15  13086  pcpremul  13101  pcdiv  13110  pcqmul  13111  pcqdiv  13115  dvdsprmpweq  13143  sumhashdc  13155  pcfaclem  13157  qexpz  13160  ballotfilemfrcn0  13331  ctinf  13379  setsvala  13441  ressressg  13488  ressabsg  13489  rngbaseg  13549  ptex  13677  issubmnd  13814  ress0g  13815  imasmnd2  13818  grpasscan2  13928  grpidrcan  13929  grpidlcan  13930  grpinvadd  13942  grpsubeq0  13950  grppncan  13955  dfgrp3m  13963  grpsubpropd2  13969  imasgrp2  13972  mhmmnd  13978  mulgnegneg  14003  mulgaddcomlem  14007  mulgaddcom  14008  mulginvcom  14009  mulgmodid  14023  issubg  14035  nsgconj  14068  nsgid  14077  quselbasg  14092  quseccl0g  14093  ghmnsgima  14130  cmn4  14198  ablinvadd  14204  ablsub4  14207  abladdsub4  14208  ablpncan2  14210  gsumsncmn  14246  gsumconstcmn  14266  pwsinvg  14322  rngpropd  14361  imasrng  14362  issrg  14376  ringidss  14441  ringcom  14443  imasring  14478  unitmulcl  14529  unitmulclb  14530  dvrcl  14551  unitdvcl  14552  dvrcan1  14556  dvrcan3  14557  issubrng  14616  subrngpropd  14633  rrgeq0  14682  islmod  14736  lmodcom  14779  rmodislmodlem  14796  rmodislmod  14797  lss0cl  14815  lssvnegcl  14822  lssintclm  14830  lssincl  14831  lspss  14845  lspun  14848  lspsnvsi  14864  lsslsp  14875  rnglidlmmgm  14942  rnglidlmsgrp  14943  rnglidlrng  14944  qus2idrng  14971  qusmulrng  14978  assa2ass  15118  assa2ass2  15119  aspid  15126  aspss  15128  asclmul1  15138  asclmul2  15139  asclinvg  15141  psrbaglecl  15169  psrbagcon  15171  2basgeng  15308  clsss  15344  ntrss  15345  ntrin  15350  neiss  15376  restco  15400  restabs  15401  lmconst  15442  psmetsym  15555  psmetge0  15557  xmetge0  15591  xmetsym  15594  xmetresbl  15666  mopni3  15710  bdxmet  15727  bdmopn  15730  txmetcnp  15744  dvfvalap  15907  dvid  15921  dvidre  15923  dvcnp2cntop  15925  elplyr  15966  ply1term  15969  ptolemy  16051  logfac  16126  rpcxpadd  16138  rpmulcxp  16142  rpdivcxp  16144  cxpmul  16145  rpcxple2  16153  rpcxplt2  16154  cxpcom  16173  rplogbval  16181  rplogbcl  16182  rprelogbmulexp  16192  relogbexpap  16194  logbleb  16197  logblt  16198  rplogbcxp  16199  rpcxplogb  16200  sgmppw  16286  prmefexple  16308  lgslem1  16324  lgsfcl2  16330  lgsneg  16348  lgsne0  16362  lgssq2  16365  lgsdirnn0  16371  gausslemma2dlem1a  16382  lgsquad  16404  2lgsoddprmlem2  16430  funvtxvalg  16482  funiedgvalg  16483  lpvtx  16525  upgrex  16549  subumgredg2en  16717  iedginwlk  16803  eulerpathprum  16926  dichmul0or  16965