Theorem simp1 1024

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simpl1  1027  simpr1  1030  simp1i  1033  simp1d  1036  simp11  1054  simp21  1057  simp31  1060  syld3an3  1319  3ianorr  1346  intn3an1d  1393  stoic4a  1477  stoic4b  1478  rsp2e  2593  ifnetruedc  3666  issod  4440  elirr  4663  sotri2  5160  sotri3  5161  funtpg  5407  funimaexglem  5439  feq123  5500  ftpg  5868  fsnunf  5884  foco2  5926  fcofo  5957  f1oiso2  6000  riotass  6033  ovmpox  6182  ovmpoga  6183  caovimo  6248  ofeq  6269  ofrval  6277  fvn0elsuppb  6452  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  frecsuclem  6637  frecrdg  6639  domssr  7017  mapxpen  7101  diffifi  7151  unsnfidcex  7180  unsnfidcel  7181  unfidisj  7182  undifdc  7184  ssfidc  7198  iunfidisj  7213  fissfi  7216  sbthlemi9  7235  elfir  7260  djuassen  7524  dftap2  7565  mulcanenq  7700  ltanqg  7715  addnnnq0  7764  distrlem4prl  7899  distrlem4pru  7900  distrprg  7903  aptipr  7956  addsrpr  8060  mulsrpr  8061  mulasssrg  8073  ltpsrprg  8118  axmulass  8188  axpre-ltadd  8201  mul31  8404  addsubass  8483  subcan2  8498  subsub2  8501  subsub4  8506  npncan3  8511  pnpcan  8512  pnncan  8514  subcan  8528  subdi  8658  ltadd1  8703  leadd1  8704  leadd2  8705  ltsubadd  8706  lesubadd  8708  ltaddsub  8710  leaddsub  8712  lesub1  8730  lesub2  8731  ltsub1  8732  ltsub2  8733  ltaddsublt  8845  gt0add  8847  apreap  8861  lemul1  8867  reapmul1lem  8868  reapmul1  8869  reapadd1  8870  remulext1  8873  remulext2  8874  apadd2  8883  mulext2  8887  mulap0r  8889  leltap  8899  ltap  8907  apsub1  8916  recexaplem2  8926  mulcanap  8939  mulcanap2  8940  divvalap  8948  divcanap2  8954  diveqap0  8956  divrecap  8962  divrecap2  8963  divdirap  8971  divcanap3  8972  div11ap  8974  muldivdirap  8981  divcanap5  8988  redivclap  9005  div2negap  9009  apmul1  9062  apmul2  9063  div2subap  9111  ltdiv1  9142  ltmuldiv  9148  lemuldiv  9155  lt2msq1  9159  ltdiv23  9166  lediv23  9167  squeeze0  9178  ofnegsub  9236  difgtsumgt  9647  gtndiv  9673  eluz2  9859  eluzsub  9884  peano2uz  9915  nn01to3  9949  divge1  10056  ledivge1le  10059  addlelt  10101  xaddass  10202  xleadd1  10208  xltadd1  10209  ixxssixx  10235  lbico1  10263  lbicc2  10317  icoshftf1o  10324  fzen  10377  fzrev3  10421  fzrevral2  10440  nelfzo  10486  elfzo0  10520  elfzo0z  10523  fzosplitprm1  10580  qbtwnre  10616  flqwordi  10648  flqword2  10649  adddivflid  10652  flltdivnn0lt  10664  modqcl  10688  mulqmod0  10692  modqmulnn  10704  modqabs2  10720  addmodid  10734  modifeq2int  10748  modqeqmodmin  10756  seqeq2  10813  seqeq3  10814  seq1g  10825  seqp1g  10828  exp3val  10903  expnegap0  10909  expgt1  10939  exprecap  10942  leexp2a  10954  expubnd  10958  sqdivap  10965  expnbnd  11025  mulsubdivbinom2ap  11073  bccmpl  11116  fihashss  11181  leisorel  11209  ccatass  11296  ccats1val2  11328  swrdval  11340  swrdval2  11343  swrdlen2  11354  swrdfv2  11355  pfxfv  11376  pfxn0  11380  pfxnd  11381  swrdswrd  11397  pfxswrd  11398  pfxpfx  11400  ccats1pfxeqbi  11434  s3cl  11478  s3fv0g  11483  s3fv1g  11484  s3fv2g  11485  shftfibg  11505  mulreap  11549  abssubne0  11776  maxleast  11898  lemininf  11919  ltmininf  11920  xrmaxltsup  11943  xrmaxaddlem  11945  xrmaxadd  11946  xrmineqinf  11954  xrltmininf  11955  xrminltinf  11957  xrminadd  11960  climuni  11978  reccn2ap  11998  isumz  12075  fsumsplitsnun  12105  geoisum1c  12206  prod1dc  12272  efltim  12384  dvdscmulr  12506  dvdsmulcr  12507  summodnegmod  12508  modmulconst  12509  dvdsmultr2  12519  dvdsexp  12547  mulmoddvds  12549  modremain  12615  divgcdz  12667  gcdaddm  12680  dvdsgcdb  12709  gcdass  12711  mulgcd  12712  gcddiv  12715  rplpwr  12723  uzwodc  12733  lcmdvdsb  12781  lcmass  12782  mulgcddvds  12791  qredeq  12793  qredeu  12794  rpmul  12795  divgcdcoprmex  12799  cncongr1  12800  rpexp  12850  rpexp12i  12852  odzcllem  12940  odzdvds  12943  odzphi  12944  pythagtriplem15  12976  pcpremul  12991  pcdiv  13000  pcqmul  13001  pcqdiv  13005  dvdsprmpweq  13033  sumhashdc  13045  pcfaclem  13047  qexpz  13050  ctinf  13181  setsvala  13243  ressressg  13288  ressabsg  13289  rngbaseg  13349  ptex  13477  issubmnd  13655  ress0g  13656  imasmnd2  13665  gsumfzz  13708  grpasscan2  13777  grpidrcan  13778  grpidlcan  13779  grpinvadd  13791  grpsubeq0  13799  grppncan  13804  dfgrp3m  13812  grpsubpropd2  13818  pwsinvg  13825  imasgrp2  13827  mhmmnd  13833  mulgnegneg  13858  mulgaddcomlem  13862  mulgaddcom  13863  mulginvcom  13864  mulgmodid  13878  issubg  13890  nsgconj  13923  nsgid  13932  quselbasg  13947  quseccl0g  13948  ghmnsgima  13985  cmn4  14022  ablinvadd  14027  ablsub4  14030  abladdsub4  14031  ablpncan2  14033  rngpropd  14099  imasrng  14100  issrg  14109  ringidss  14173  ringcom  14175  imasring  14208  unitmulcl  14258  unitmulclb  14259  dvrcl  14280  unitdvcl  14281  dvrcan1  14285  dvrcan3  14286  issubrng  14344  subrngpropd  14361  rrgeq0  14410  islmod  14439  lmodcom  14481  rmodislmodlem  14498  rmodislmod  14499  lss0cl  14517  lssvnegcl  14524  lssintclm  14532  lssincl  14533  lspss  14547  lspun  14550  lspsnvsi  14566  lsslsp  14577  rnglidlmmgm  14644  rnglidlmsgrp  14645  rnglidlrng  14646  qus2idrng  14673  qusmulrng  14680  psrbaglecl  14824  psrbagcon  14826  2basgeng  14947  clsss  14983  ntrss  14984  ntrin  14989  neiss  15015  restco  15039  restabs  15040  lmconst  15081  psmetsym  15194  psmetge0  15196  xmetge0  15230  xmetsym  15233  xmetresbl  15305  mopni3  15349  bdxmet  15366  bdmopn  15369  txmetcnp  15383  dvfvalap  15546  dvid  15560  dvidre  15562  dvcnp2cntop  15564  elplyr  15605  ply1term  15608  ptolemy  15689  rpcxpadd  15770  rpmulcxp  15774  rpdivcxp  15776  cxpmul  15777  rpcxple2  15783  rpcxplt2  15784  cxpcom  15803  rplogbval  15810  rplogbcl  15811  rprelogbmulexp  15821  relogbexpap  15823  logbleb  15826  logblt  15827  rplogbcxp  15828  rpcxplogb  15829  sgmppw  15860  lgslem1  15873  lgsfcl2  15879  lgsneg  15897  lgsne0  15911  lgssq2  15914  lgsdirnn0  15920  gausslemma2dlem1a  15931  lgsquad  15953  2lgsoddprmlem2  15979  funvtxvalg  16031  funiedgvalg  16032  lpvtx  16074  upgrex  16098  subumgredg2en  16266  iedginwlk  16352  eulerpathprum  16475  gfsumsn  16867