Theorem simp1 962

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

Syntax hints:   -> wi 4   /\ w3a 943

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 945

This theorem is referenced by:  simpl1  965  simpr1  968  simp1i  971  simp1d  974  simp11  992  simp21  995  simp31  998  syld3an3  1242  3ianorr  1268  stoic4a  1389  stoic4b  1390  rsp2e  2455  issod  4199  elirr  4414  sotri2  4892  sotri3  4893  funtpg  5130  funimaexglem  5162  feq123  5220  ftpg  5556  fsnunf  5572  foco2  5607  fcofo  5637  f1oiso2  5680  riotass  5709  ovmpox  5851  ovmpoga  5852  caovimo  5916  ofeq  5936  ofrval  5944  tfr1onlembxssdm  6192  tfrcllembxssdm  6205  frecsuclem  6255  frecrdg  6257  mapxpen  6693  diffifi  6739  unsnfidcex  6759  unsnfidcel  6760  unfidisj  6761  undifdc  6763  ssfidc  6773  iunfidisj  6784  sbthlemi9  6803  elfir  6811  djuassen  7018  mulcanenq  7135  ltanqg  7150  addnnnq0  7199  distrlem4prl  7334  distrlem4pru  7335  distrprg  7338  aptipr  7391  addsrpr  7482  mulsrpr  7483  mulasssrg  7495  axmulass  7602  axpre-ltadd  7615  mul31  7810  addsubass  7889  subcan2  7904  subsub2  7907  subsub4  7912  npncan3  7917  pnpcan  7918  pnncan  7920  subcan  7934  subdi  8060  ltadd1  8104  leadd1  8105  leadd2  8106  ltsubadd  8107  lesubadd  8109  ltaddsub  8111  leaddsub  8113  lesub1  8131  lesub2  8132  ltsub1  8133  ltsub2  8134  ltaddsublt  8245  gt0add  8247  apreap  8261  lemul1  8267  reapmul1lem  8268  reapmul1  8269  reapadd1  8270  remulext1  8273  remulext2  8274  apadd2  8283  mulext2  8287  mulap0r  8289  leltap  8299  ltap  8306  apsub1  8315  recexaplem2  8320  mulcanap  8333  mulcanap2  8334  divvalap  8341  divcanap2  8347  diveqap0  8349  divrecap  8355  divrecap2  8356  divdirap  8364  divcanap3  8365  div11ap  8367  muldivdirap  8374  divcanap5  8381  redivclap  8398  div2negap  8402  apmul1  8455  apmul2  8456  div2subap  8503  ltdiv1  8530  ltmuldiv  8536  lemuldiv  8543  lt2msq1  8547  ltdiv23  8554  lediv23  8555  squeeze0  8566  gtndiv  9044  eluz2  9228  eluzsub  9251  peano2uz  9274  nn01to3  9305  divge1  9403  ledivge1le  9406  addlelt  9442  xaddass  9539  xleadd1  9545  xltadd1  9546  ixxssixx  9572  lbico1  9600  lbicc2  9654  icoshftf1o  9661  fzen  9710  fzrev3  9754  fzrevral2  9773  elfzo0  9846  elfzo0z  9848  fzosplitprm1  9898  qbtwnre  9921  flqwordi  9948  flqword2  9949  adddivflid  9952  flltdivnn0lt  9964  modqcl  9986  mulqmod0  9990  modqmulnn  10002  modqabs2  10018  addmodid  10032  modifeq2int  10046  modqeqmodmin  10054  seqeq2  10109  seqeq3  10110  exp3val  10182  expnegap0  10188  expgt1  10218  exprecap  10221  leexp2a  10233  expubnd  10237  sqdivap  10244  expnbnd  10302  bccmpl  10387  fihashss  10449  leisorel  10467  shftfibg  10479  mulreap  10523  abssubne0  10749  maxleast  10871  lemininf  10891  ltmininf  10892  xrmaxltsup  10913  xrmaxaddlem  10915  xrmaxadd  10916  xrmineqinf  10924  xrltmininf  10925  xrminltinf  10927  xrminadd  10930  climuni  10948  reccn2ap  10968  isumz  11044  fsumsplitsnun  11074  geoisum1c  11175  efltim  11249  dvdscmulr  11364  dvdsmulcr  11365  summodnegmod  11366  modmulconst  11367  dvdsmultr2  11375  dvdsexp  11401  mulmoddvds  11403  modremain  11468  divgcdz  11502  gcdaddm  11514  dvdsgcdb  11541  gcdass  11543  mulgcd  11544  gcddiv  11547  rplpwr  11555  lcmdvdsb  11605  lcmass  11606  mulgcddvds  11615  qredeq  11617  qredeu  11618  rpmul  11619  divgcdcoprmex  11623  cncongr1  11624  rpexp  11671  rpexp12i  11673  ctinf  11782  setsvala  11827  ressid2  11855  ressval2  11856  rngbaseg  11912  2basgeng  12088  clsss  12124  ntrss  12125  ntrin  12130  neiss  12156  restco  12180  restabs  12181  lmconst  12221  psmetsym  12312  psmetge0  12314  xmetge0  12348  xmetsym  12351  xmetresbl  12423  mopni3  12467  bdxmet  12484  bdmopn  12487  txmetcnp  12501  dvfvalap  12599  dvid  12611  dvcnp2cntop  12612