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  2595  ifnetruedc  3670  issod  4445  elirr  4668  sotri2  5165  sotri3  5166  funtpg  5412  funimaexglem  5444  feq123  5505  ftpg  5873  fsnunf  5889  foco2  5932  fcofo  5963  f1oiso2  6006  riotass  6041  ovmpox  6190  ovmpoga  6191  caovimo  6256  ofeq  6278  ofrval  6286  fvn0elsuppb  6465  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  frecsuclem  6650  frecrdg  6652  domssr  7030  mapxpen  7114  diffifi  7164  unsnfidcex  7193  unsnfidcel  7194  unfidisj  7195  undifdc  7197  ssfidc  7211  iunfidisj  7226  fissfi  7229  sbthlemi9  7248  elfir  7273  djuassen  7537  dftap2  7581  mulcanenq  7716  ltanqg  7731  addnnnq0  7780  distrlem4prl  7915  distrlem4pru  7916  distrprg  7919  aptipr  7972  addsrpr  8076  mulsrpr  8077  mulasssrg  8089  ltpsrprg  8134  axmulass  8204  axpre-ltadd  8217  mul31  8420  addsubass  8499  subcan2  8514  subsub2  8517  subsub4  8522  npncan3  8527  pnpcan  8528  pnncan  8530  subcan  8544  subdi  8675  ltadd1  8720  leadd1  8721  leadd2  8722  ltsubadd  8723  lesubadd  8725  ltaddsub  8727  leaddsub  8729  lesub1  8747  lesub2  8748  ltsub1  8749  ltsub2  8750  ltaddsublt  8862  gt0add  8864  apreap  8878  lemul1  8884  reapmul1lem  8885  reapmul1  8886  reapadd1  8887  remulext1  8890  remulext2  8891  apadd2  8900  mulext2  8904  mulap0r  8906  leltap  8916  ltap  8924  apsub1  8933  recexaplem2  8943  mulcanap  8956  mulcanap2  8957  divvalap  8965  divcanap2  8971  diveqap0  8973  divrecap  8979  divrecap2  8980  divdirap  8988  divcanap3  8989  div11ap  8991  muldivdirap  8998  divcanap5  9005  redivclap  9022  div2negap  9026  apmul1  9079  apmul2  9080  div2subap  9128  ltdiv1  9159  ltmuldiv  9165  lemuldiv  9172  lt2msq1  9176  ltdiv23  9183  lediv23  9184  squeeze0  9195  ofnegsub  9253  difgtsumgt  9664  zfidc  9673  gtndiv  9691  eluz2  9877  eluzsub  9902  peano2uz  9933  nn01to3  9967  divge1  10074  ledivge1le  10077  addlelt  10119  xaddass  10221  xleadd1  10227  xltadd1  10228  ixxssixx  10254  lbico1  10282  lbicc2  10336  icoshftf1o  10343  fzen  10397  fzrev3  10443  fzrevral2  10462  nelfzo  10508  elfzo0  10542  elfzo0z  10545  fzosplitprm1  10602  qbtwnre  10640  flqwordi  10672  flqword2  10673  adddivflid  10676  flltdivnn0lt  10688  modqcl  10712  mulqmod0  10716  modqmulnn  10728  modqabs2  10744  addmodid  10758  modifeq2int  10772  modqeqmodmin  10780  seqeq2  10837  seqeq3  10838  seq1g  10849  seqp1g  10852  exp3val  10927  expnegap0  10933  expgt1  10963  exprecap  10966  leexp2a  10978  expubnd  10982  sqdivap  10989  expnbnd  11050  mulsubdivbinom2ap  11098  bccmpl  11141  fihashss  11206  leisorel  11234  ccatass  11321  ccats1val2  11353  swrdval  11365  swrdval2  11368  swrdlen2  11379  swrdfv2  11380  pfxfv  11401  pfxn0  11405  pfxnd  11406  swrdswrd  11422  pfxswrd  11423  pfxpfx  11425  ccats1pfxeqbi  11459  s3cl  11503  s3fv0g  11508  s3fv1g  11509  s3fv2g  11510  shftfibg  11530  mulreap  11574  abssubne0  11801  maxleast  11923  lemininf  11944  ltmininf  11945  xrmaxltsup  11968  xrmaxaddlem  11970  xrmaxadd  11971  xrmineqinf  11979  xrltmininf  11980  xrminltinf  11982  xrminadd  11985  climuni  12003  reccn2ap  12023  isumz  12100  fsumsplitsnun  12130  geoisum1c  12231  prod1dc  12297  efltim  12409  dvdscmulr  12531  dvdsmulcr  12532  summodnegmod  12533  modmulconst  12534  dvdsmultr2  12544  dvdsexp  12572  mulmoddvds  12574  modremain  12640  divgcdz  12692  gcdaddm  12705  dvdsgcdb  12734  gcdass  12736  mulgcd  12737  gcddiv  12740  rplpwr  12748  uzwodc  12758  lcmdvdsb  12806  lcmass  12807  mulgcddvds  12816  qredeq  12818  qredeu  12819  rpmul  12820  divgcdcoprmex  12824  cncongr1  12825  rpexp  12875  rpexp12i  12877  odzcllem  12965  odzdvds  12968  odzphi  12969  pythagtriplem15  13001  pcpremul  13016  pcdiv  13025  pcqmul  13026  pcqdiv  13030  dvdsprmpweq  13058  sumhashdc  13070  pcfaclem  13072  qexpz  13075  ballotfilemfrcn0  13217  ctinf  13265  setsvala  13327  ressressg  13372  ressabsg  13373  rngbaseg  13433  ptex  13561  issubmnd  13703  ress0g  13704  imasmnd2  13707  gsumfzz  13750  grpasscan2  13819  grpidrcan  13820  grpidlcan  13821  grpinvadd  13833  grpsubeq0  13841  grppncan  13846  dfgrp3m  13854  grpsubpropd2  13860  imasgrp2  13863  mhmmnd  13869  mulgnegneg  13894  mulgaddcomlem  13898  mulgaddcom  13899  mulginvcom  13900  mulgmodid  13914  issubg  13926  nsgconj  13959  nsgid  13968  quselbasg  13983  quseccl0g  13984  ghmnsgima  14021  cmn4  14058  ablinvadd  14063  ablsub4  14066  abladdsub4  14067  ablpncan2  14069  gfsumsn  14107  pwsinvg  14157  rngpropd  14194  imasrng  14195  issrg  14208  ringidss  14272  ringcom  14274  imasring  14307  unitmulcl  14358  unitmulclb  14359  dvrcl  14380  unitdvcl  14381  dvrcan1  14385  dvrcan3  14386  issubrng  14445  subrngpropd  14462  rrgeq0  14511  islmod  14565  lmodcom  14607  rmodislmodlem  14624  rmodislmod  14625  lss0cl  14643  lssvnegcl  14650  lssintclm  14658  lssincl  14659  lspss  14673  lspun  14676  lspsnvsi  14692  lsslsp  14703  rnglidlmmgm  14770  rnglidlmsgrp  14771  rnglidlrng  14772  qus2idrng  14799  qusmulrng  14806  psrbaglecl  14950  psrbagcon  14952  2basgeng  15073  clsss  15109  ntrss  15110  ntrin  15115  neiss  15141  restco  15165  restabs  15166  lmconst  15207  psmetsym  15320  psmetge0  15322  xmetge0  15356  xmetsym  15359  xmetresbl  15431  mopni3  15475  bdxmet  15492  bdmopn  15495  txmetcnp  15509  dvfvalap  15672  dvid  15686  dvidre  15688  dvcnp2cntop  15690  elplyr  15731  ply1term  15734  ptolemy  15815  rpcxpadd  15896  rpmulcxp  15900  rpdivcxp  15902  cxpmul  15903  rpcxple2  15909  rpcxplt2  15910  cxpcom  15929  rplogbval  15936  rplogbcl  15937  rprelogbmulexp  15947  relogbexpap  15949  logbleb  15952  logblt  15953  rplogbcxp  15954  rpcxplogb  15955  sgmppw  15986  lgslem1  15999  lgsfcl2  16005  lgsneg  16023  lgsne0  16037  lgssq2  16040  lgsdirnn0  16046  gausslemma2dlem1a  16057  lgsquad  16079  2lgsoddprmlem2  16105  funvtxvalg  16157  funiedgvalg  16158  lpvtx  16200  upgrex  16224  subumgredg2en  16392  iedginwlk  16478  eulerpathprum  16601