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  6619  tfrcllembxssdm  6632  frecsuclem  6682  frecrdg  6684  mapm  6975  domssr  7070  mapxpen  7154  diffifi  7204  unsnfidcex  7233  unsnfidcel  7234  unfidisj  7235  undifdc  7237  ssfidc  7251  iunfidisj  7266  fissfi  7269  sbthlemi9  7289  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  9723  zfidc  9732  gtndiv  9751  eluz2  9942  eluzsub  9967  peano2uz  9998  nn01to3  10032  divge1  10140  ledivge1le  10143  addlelt  10185  xaddass  10287  xleadd1  10293  xltadd1  10294  ixxssixx  10320  lbico1  10348  lbicc2  10402  icoshftf1o  10409  fzen  10463  fzrev3  10510  fzrevral2  10529  nelfzo  10575  elfzo0  10609  elfzo0z  10612  fzosplitprm1  10669  qbtwnre  10707  flqwordi  10743  flqword2  10744  adddivflid  10747  flltdivnn0lt  10759  modqcl  10783  mulqmod0  10787  modqmulnn  10799  modqabs2  10815  addmodid  10829  modifeq2int  10843  modqeqmodmin  10851  seqeq2  10908  seqeq3  10909  seq1g  10920  seqp1g  10923  exp3val  10998  expnegap0  11004  expgt1  11034  exprecap  11037  leexp2a  11049  expubnd  11053  sqdivap  11060  expnbnd  11121  mulsubdivbinom2ap  11170  bccmpl  11213  fihashss  11278  leisorel  11310  ccatass  11397  ccats1val2  11429  swrdval  11441  swrdval2  11444  swrdlen2  11455  swrdfv2  11456  pfxfv  11477  pfxn0  11481  pfxnd  11482  swrdswrd  11498  pfxswrd  11499  pfxpfx  11501  ccats1pfxeqbi  11535  s3cl  11579  s3fv0g  11584  s3fv1g  11585  s3fv2g  11586  shftfibg  11606  mulreap  11650  abssubne0  11879  maxleast  12001  lemininf  12023  ltmininf  12024  xrmaxltsup  12048  xrmaxaddlem  12050  xrmaxadd  12051  xrmineqinf  12059  xrltmininf  12060  xrminltinf  12062  xrminadd  12065  climuni  12083  reccn2ap  12103  isumz  12180  fsumsplitsnun  12210  geoisum1c  12311  prod1dc  12377  efltim  12489  dvdscmulr  12611  dvdsmulcr  12612  summodnegmod  12613  modmulconst  12614  dvdsmultr2  12624  dvdsexp  12652  mulmoddvds  12654  modremain  12720  divgcdz  12772  gcdaddm  12785  dvdsgcdb  12814  gcdass  12816  mulgcd  12817  gcddiv  12820  rplpwr  12828  uzwodc  12838  lcmdvdsb  12886  lcmass  12887  mulgcddvds  12896  qredeq  12898  qredeu  12899  rpmul  12900  divgcdcoprmex  12904  cncongr1  12905  rpexp  12956  rpexp12i  12958  odzcllem  13049  odzdvds  13052  odzphi  13053  pythagtriplem15  13085  pcpremul  13100  pcdiv  13109  pcqmul  13110  pcqdiv  13114  dvdsprmpweq  13142  sumhashdc  13154  pcfaclem  13156  qexpz  13159  ballotfilemfrcn0  13330  ctinf  13378  setsvala  13440  ressressg  13487  ressabsg  13488  rngbaseg  13548  ptex  13676  issubmnd  13813  ress0g  13814  imasmnd2  13817  grpasscan2  13927  grpidrcan  13928  grpidlcan  13929  grpinvadd  13941  grpsubeq0  13949  grppncan  13954  dfgrp3m  13962  grpsubpropd2  13968  imasgrp2  13971  mhmmnd  13977  mulgnegneg  14002  mulgaddcomlem  14006  mulgaddcom  14007  mulginvcom  14008  mulgmodid  14022  issubg  14034  nsgconj  14067  nsgid  14076  quselbasg  14091  quseccl0g  14092  ghmnsgima  14129  cmn4  14197  ablinvadd  14203  ablsub4  14206  abladdsub4  14207  ablpncan2  14209  gsumsncmn  14245  gsumconstcmn  14265  pwsinvg  14321  rngpropd  14360  imasrng  14361  issrg  14375  ringidss  14440  ringcom  14442  imasring  14477  unitmulcl  14528  unitmulclb  14529  dvrcl  14550  unitdvcl  14551  dvrcan1  14555  dvrcan3  14556  issubrng  14615  subrngpropd  14632  rrgeq0  14681  islmod  14735  lmodcom  14778  rmodislmodlem  14795  rmodislmod  14796  lss0cl  14814  lssvnegcl  14821  lssintclm  14829  lssincl  14830  lspss  14844  lspun  14847  lspsnvsi  14863  lsslsp  14874  rnglidlmmgm  14941  rnglidlmsgrp  14942  rnglidlrng  14943  qus2idrng  14970  qusmulrng  14977  assa2ass  15117  assa2ass2  15118  aspid  15125  aspss  15127  asclmul1  15137  asclmul2  15138  asclinvg  15140  psrbagdceq  15167  snifpsrbagfi  15168  psrbaglecl  15172  psrbagcon  15174  2basgeng  15325  clsss  15361  ntrss  15362  ntrin  15367  neiss  15393  restco  15417  restabs  15418  lmconst  15459  psmetsym  15572  psmetge0  15574  xmetge0  15608  xmetsym  15611  xmetresbl  15683  mopni3  15727  bdxmet  15744  bdmopn  15747  txmetcnp  15761  dvfvalap  15924  dvid  15938  dvidre  15940  dvcnp2cntop  15942  elplyr  15983  ply1term  15986  ptolemy  16068  logfac  16143  rpcxpadd  16155  rpmulcxp  16159  rpdivcxp  16161  cxpmul  16162  rpcxple2  16170  rpcxplt2  16171  cxpcom  16190  rplogbval  16198  rplogbcl  16199  rprelogbmulexp  16209  relogbexpap  16211  logbleb  16214  logblt  16215  rplogbcxp  16216  rpcxplogb  16217  sgmppw  16303  prmefexple  16325  lgslem1  16341  lgsfcl2  16347  lgsneg  16365  lgsne0  16379  lgssq2  16382  lgsdirnn0  16388  gausslemma2dlem1a  16399  lgsquad  16421  2lgsoddprmlem2  16447  funvtxvalg  16499  funiedgvalg  16500  lpvtx  16542  upgrex  16566  subumgredg2en  16734  iedginwlk  16820  eulerpathprum  16943  dichmul0or  16982