Theorem simp1 1021

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simpl1  1024  simpr1  1027  simp1i  1030  simp1d  1033  simp11  1051  simp21  1054  simp31  1057  syld3an3  1316  3ianorr  1343  intn3an1d  1390  stoic4a  1474  stoic4b  1475  rsp2e  2581  ifnetruedc  3646  issod  4410  elirr  4633  sotri2  5126  sotri3  5127  funtpg  5372  funimaexglem  5404  feq123  5465  ftpg  5823  fsnunf  5839  foco2  5877  fcofo  5908  f1oiso2  5951  riotass  5984  ovmpox  6133  ovmpoga  6134  caovimo  6199  ofeq  6221  ofrval  6229  tfr1onlembxssdm  6489  tfrcllembxssdm  6502  frecsuclem  6552  frecrdg  6554  domssr  6929  mapxpen  7009  diffifi  7056  unsnfidcex  7082  unsnfidcel  7083  unfidisj  7084  undifdc  7086  ssfidc  7099  iunfidisj  7113  sbthlemi9  7132  elfir  7140  djuassen  7399  dftap2  7437  mulcanenq  7572  ltanqg  7587  addnnnq0  7636  distrlem4prl  7771  distrlem4pru  7772  distrprg  7775  aptipr  7828  addsrpr  7932  mulsrpr  7933  mulasssrg  7945  ltpsrprg  7990  axmulass  8060  axpre-ltadd  8073  mul31  8277  addsubass  8356  subcan2  8371  subsub2  8374  subsub4  8379  npncan3  8384  pnpcan  8385  pnncan  8387  subcan  8401  subdi  8531  ltadd1  8576  leadd1  8577  leadd2  8578  ltsubadd  8579  lesubadd  8581  ltaddsub  8583  leaddsub  8585  lesub1  8603  lesub2  8604  ltsub1  8605  ltsub2  8606  ltaddsublt  8718  gt0add  8720  apreap  8734  lemul1  8740  reapmul1lem  8741  reapmul1  8742  reapadd1  8743  remulext1  8746  remulext2  8747  apadd2  8756  mulext2  8760  mulap0r  8762  leltap  8772  ltap  8780  apsub1  8789  recexaplem2  8799  mulcanap  8812  mulcanap2  8813  divvalap  8821  divcanap2  8827  diveqap0  8829  divrecap  8835  divrecap2  8836  divdirap  8844  divcanap3  8845  div11ap  8847  muldivdirap  8854  divcanap5  8861  redivclap  8878  div2negap  8882  apmul1  8935  apmul2  8936  div2subap  8984  ltdiv1  9015  ltmuldiv  9021  lemuldiv  9028  lt2msq1  9032  ltdiv23  9039  lediv23  9040  squeeze0  9051  ofnegsub  9109  difgtsumgt  9516  gtndiv  9542  eluz2  9728  eluzsub  9752  peano2uz  9778  nn01to3  9812  divge1  9919  ledivge1le  9922  addlelt  9964  xaddass  10065  xleadd1  10071  xltadd1  10072  ixxssixx  10098  lbico1  10126  lbicc2  10180  icoshftf1o  10187  fzen  10239  fzrev3  10283  fzrevral2  10302  nelfzo  10348  elfzo0  10382  elfzo0z  10384  fzosplitprm1  10440  qbtwnre  10476  flqwordi  10508  flqword2  10509  adddivflid  10512  flltdivnn0lt  10524  modqcl  10548  mulqmod0  10552  modqmulnn  10564  modqabs2  10580  addmodid  10594  modifeq2int  10608  modqeqmodmin  10616  seqeq2  10673  seqeq3  10674  seq1g  10685  seqp1g  10688  exp3val  10763  expnegap0  10769  expgt1  10799  exprecap  10802  leexp2a  10814  expubnd  10818  sqdivap  10825  expnbnd  10885  mulsubdivbinom2ap  10933  bccmpl  10976  fihashss  11038  leisorel  11059  ccatass  11143  ccats1val2  11171  swrdval  11180  swrdval2  11183  swrdlen2  11194  swrdfv2  11195  pfxfv  11216  pfxn0  11220  pfxnd  11221  swrdswrd  11237  pfxswrd  11238  pfxpfx  11240  ccats1pfxeqbi  11274  s3cl  11318  s3fv0g  11323  s3fv1g  11324  shftfibg  11331  mulreap  11375  abssubne0  11602  maxleast  11724  lemininf  11745  ltmininf  11746  xrmaxltsup  11769  xrmaxaddlem  11771  xrmaxadd  11772  xrmineqinf  11780  xrltmininf  11781  xrminltinf  11783  xrminadd  11786  climuni  11804  reccn2ap  11824  isumz  11900  fsumsplitsnun  11930  geoisum1c  12031  prod1dc  12097  efltim  12209  dvdscmulr  12331  dvdsmulcr  12332  summodnegmod  12333  modmulconst  12334  dvdsmultr2  12344  dvdsexp  12372  mulmoddvds  12374  modremain  12440  divgcdz  12492  gcdaddm  12505  dvdsgcdb  12534  gcdass  12536  mulgcd  12537  gcddiv  12540  rplpwr  12548  uzwodc  12558  lcmdvdsb  12606  lcmass  12607  mulgcddvds  12616  qredeq  12618  qredeu  12619  rpmul  12620  divgcdcoprmex  12624  cncongr1  12625  rpexp  12675  rpexp12i  12677  odzcllem  12765  odzdvds  12768  odzphi  12769  pythagtriplem15  12801  pcpremul  12816  pcdiv  12825  pcqmul  12826  pcqdiv  12830  dvdsprmpweq  12858  sumhashdc  12870  pcfaclem  12872  qexpz  12875  ctinf  13001  setsvala  13063  ressressg  13108  ressabsg  13109  rngbaseg  13169  ptex  13297  issubmnd  13475  ress0g  13476  imasmnd2  13485  gsumfzz  13528  grpasscan2  13597  grpidrcan  13598  grpidlcan  13599  grpinvadd  13611  grpsubeq0  13619  grppncan  13624  dfgrp3m  13632  grpsubpropd2  13638  pwsinvg  13645  imasgrp2  13647  mhmmnd  13653  mulgnegneg  13678  mulgaddcomlem  13682  mulgaddcom  13683  mulginvcom  13684  mulgmodid  13698  issubg  13710  nsgconj  13743  nsgid  13752  quselbasg  13767  quseccl0g  13768  ghmnsgima  13805  cmn4  13842  ablinvadd  13847  ablsub4  13850  abladdsub4  13851  ablpncan2  13853  rngpropd  13918  imasrng  13919  issrg  13928  ringidss  13992  ringcom  13994  imasring  14027  unitmulcl  14077  unitmulclb  14078  dvrcl  14099  unitdvcl  14100  dvrcan1  14104  dvrcan3  14105  issubrng  14163  subrngpropd  14180  rrgeq0  14229  islmod  14255  lmodcom  14297  rmodislmodlem  14314  rmodislmod  14315  lss0cl  14333  lssvnegcl  14340  lssintclm  14348  lssincl  14349  lspss  14363  lspun  14366  lspsnvsi  14382  lsslsp  14393  rnglidlmmgm  14460  rnglidlmsgrp  14461  rnglidlrng  14462  qus2idrng  14489  qusmulrng  14496  2basgeng  14756  clsss  14792  ntrss  14793  ntrin  14798  neiss  14824  restco  14848  restabs  14849  lmconst  14890  psmetsym  15003  psmetge0  15005  xmetge0  15039  xmetsym  15042  xmetresbl  15114  mopni3  15158  bdxmet  15175  bdmopn  15178  txmetcnp  15192  dvfvalap  15355  dvid  15369  dvidre  15371  dvcnp2cntop  15373  elplyr  15414  ply1term  15417  ptolemy  15498  rpcxpadd  15579  rpmulcxp  15583  rpdivcxp  15585  cxpmul  15586  rpcxple2  15592  rpcxplt2  15593  cxpcom  15612  rplogbval  15619  rplogbcl  15620  rprelogbmulexp  15630  relogbexpap  15632  logbleb  15635  logblt  15636  rplogbcxp  15637  rpcxplogb  15638  sgmppw  15666  lgslem1  15679  lgsfcl2  15685  lgsneg  15703  lgsne0  15717  lgssq2  15720  lgsdirnn0  15726  gausslemma2dlem1a  15737  lgsquad  15759  2lgsoddprmlem2  15785  funvtxvalg  15837  funiedgvalg  15838  lpvtx  15879  upgrex  15903  iedginwlk  16068