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  8458  addsubass  8537  subcan2  8552  subsub2  8555  subsub4  8560  npncan3  8565  pnpcan  8566  pnncan  8568  subcan  8582  subdi  8713  ltadd1  8758  leadd1  8759  leadd2  8760  ltsubadd  8761  lesubadd  8763  ltaddsub  8765  leaddsub  8767  lesub1  8785  lesub2  8786  ltsub1  8787  ltsub2  8788  ltaddsublt  8901  gt0add  8903  apreap  8917  lemul1  8923  reapmul1lem  8924  reapmul1  8925  reapadd1  8926  remulext1  8929  remulext2  8930  apadd2  8939  mulext2  8943  mulap0r  8945  leltap  8955  ltap  8963  apsub1  8972  recexaplem2  8982  mulcanap  8995  mulcanap2  8996  divvalap  9006  divcanap2  9012  diveqap0  9014  divrecap  9020  divrecap2  9021  divdirap  9029  divcanap3  9030  div11ap  9032  muldivdirap  9039  divcanap5  9046  redivclap  9063  div2negap  9067  apmul1  9120  apmul2  9121  div2subap  9169  ltdiv1  9200  ltmuldiv  9206  lemuldiv  9213  lt2msq1  9217  ltdiv23  9224  lediv23  9225  squeeze0  9236  ofnegsub  9294  difgtsumgt  9718  zfidc  9727  gtndiv  9745  eluz2  9936  eluzsub  9961  peano2uz  9992  nn01to3  10026  divge1  10134  ledivge1le  10137  addlelt  10179  xaddass  10281  xleadd1  10287  xltadd1  10288  ixxssixx  10314  lbico1  10342  lbicc2  10396  icoshftf1o  10403  fzen  10457  fzrev3  10504  fzrevral2  10523  nelfzo  10569  elfzo0  10603  elfzo0z  10606  fzosplitprm1  10663  qbtwnre  10701  flqwordi  10736  flqword2  10737  adddivflid  10740  flltdivnn0lt  10752  modqcl  10776  mulqmod0  10780  modqmulnn  10792  modqabs2  10808  addmodid  10822  modifeq2int  10836  modqeqmodmin  10844  seqeq2  10901  seqeq3  10902  seq1g  10913  seqp1g  10916  exp3val  10991  expnegap0  10997  expgt1  11027  exprecap  11030  leexp2a  11042  expubnd  11046  sqdivap  11053  expnbnd  11114  mulsubdivbinom2ap  11163  bccmpl  11206  fihashss  11271  leisorel  11303  ccatass  11390  ccats1val2  11422  swrdval  11434  swrdval2  11437  swrdlen2  11448  swrdfv2  11449  pfxfv  11470  pfxn0  11474  pfxnd  11475  swrdswrd  11491  pfxswrd  11492  pfxpfx  11494  ccats1pfxeqbi  11528  s3cl  11572  s3fv0g  11577  s3fv1g  11578  s3fv2g  11579  shftfibg  11599  mulreap  11643  abssubne0  11872  maxleast  11994  lemininf  12015  ltmininf  12016  xrmaxltsup  12040  xrmaxaddlem  12042  xrmaxadd  12043  xrmineqinf  12051  xrltmininf  12052  xrminltinf  12054  xrminadd  12057  climuni  12075  reccn2ap  12095  isumz  12172  fsumsplitsnun  12202  geoisum1c  12303  prod1dc  12369  efltim  12481  dvdscmulr  12603  dvdsmulcr  12604  summodnegmod  12605  modmulconst  12606  dvdsmultr2  12616  dvdsexp  12644  mulmoddvds  12646  modremain  12712  divgcdz  12764  gcdaddm  12777  dvdsgcdb  12806  gcdass  12808  mulgcd  12809  gcddiv  12812  rplpwr  12820  uzwodc  12830  lcmdvdsb  12878  lcmass  12879  mulgcddvds  12888  qredeq  12890  qredeu  12891  rpmul  12892  divgcdcoprmex  12896  cncongr1  12897  rpexp  12948  rpexp12i  12950  odzcllem  13041  odzdvds  13044  odzphi  13045  pythagtriplem15  13077  pcpremul  13092  pcdiv  13101  pcqmul  13102  pcqdiv  13106  dvdsprmpweq  13134  sumhashdc  13146  pcfaclem  13148  qexpz  13151  ballotfilemfrcn0  13322  ctinf  13370  setsvala  13432  ressressg  13478  ressabsg  13479  rngbaseg  13539  ptex  13667  issubmnd  13804  ress0g  13805  imasmnd2  13808  grpasscan2  13918  grpidrcan  13919  grpidlcan  13920  grpinvadd  13932  grpsubeq0  13940  grppncan  13945  dfgrp3m  13953  grpsubpropd2  13959  imasgrp2  13962  mhmmnd  13968  mulgnegneg  13993  mulgaddcomlem  13997  mulgaddcom  13998  mulginvcom  13999  mulgmodid  14013  issubg  14025  nsgconj  14058  nsgid  14067  quselbasg  14082  quseccl0g  14083  ghmnsgima  14120  cmn4  14157  ablinvadd  14163  ablsub4  14166  abladdsub4  14167  ablpncan2  14169  gsumsncmn  14205  gsumconstcmn  14215  pwsinvg  14264  rngpropd  14303  imasrng  14304  issrg  14318  ringidss  14383  ringcom  14385  imasring  14418  unitmulcl  14469  unitmulclb  14470  dvrcl  14491  unitdvcl  14492  dvrcan1  14496  dvrcan3  14497  issubrng  14556  subrngpropd  14573  rrgeq0  14622  islmod  14676  lmodcom  14719  rmodislmodlem  14736  rmodislmod  14737  lss0cl  14755  lssvnegcl  14762  lssintclm  14770  lssincl  14771  lspss  14785  lspun  14788  lspsnvsi  14804  lsslsp  14815  rnglidlmmgm  14882  rnglidlmsgrp  14883  rnglidlrng  14884  qus2idrng  14911  qusmulrng  14918  assa2ass  15058  assa2ass2  15059  aspid  15066  aspss  15068  asclmul1  15078  asclmul2  15079  asclinvg  15081  psrbaglecl  15109  psrbagcon  15111  2basgeng  15232  clsss  15268  ntrss  15269  ntrin  15274  neiss  15300  restco  15324  restabs  15325  lmconst  15366  psmetsym  15479  psmetge0  15481  xmetge0  15515  xmetsym  15518  xmetresbl  15590  mopni3  15634  bdxmet  15651  bdmopn  15654  txmetcnp  15668  dvfvalap  15831  dvid  15845  dvidre  15847  dvcnp2cntop  15849  elplyr  15890  ply1term  15893  ptolemy  15975  logfac  16048  rpcxpadd  16060  rpmulcxp  16064  rpdivcxp  16066  cxpmul  16067  rpcxple2  16073  rpcxplt2  16074  cxpcom  16093  rplogbval  16100  rplogbcl  16101  rprelogbmulexp  16111  relogbexpap  16113  logbleb  16116  logblt  16117  rplogbcxp  16118  rpcxplogb  16119  sgmppw  16187  prmefexple  16206  lgslem1  16217  lgsfcl2  16223  lgsneg  16241  lgsne0  16255  lgssq2  16258  lgsdirnn0  16264  gausslemma2dlem1a  16275  lgsquad  16297  2lgsoddprmlem2  16323  funvtxvalg  16375  funiedgvalg  16376  lpvtx  16418  upgrex  16442  subumgredg2en  16610  iedginwlk  16696  eulerpathprum  16819  dichmul0or  16858