Theorem simp1 1000

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

Syntax hints:   -> wi 4   /\ w3a 981

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 983

This theorem is referenced by:  simpl1  1003  simpr1  1006  simp1i  1009  simp1d  1012  simp11  1030  simp21  1033  simp31  1036  syld3an3  1295  3ianorr  1322  intn3an1d  1368  stoic4a  1452  stoic4b  1453  rsp2e  2557  ifnetruedc  3613  issod  4366  elirr  4589  sotri2  5080  sotri3  5081  funtpg  5325  funimaexglem  5357  feq123  5417  ftpg  5768  fsnunf  5784  foco2  5822  fcofo  5853  f1oiso2  5896  riotass  5927  ovmpox  6074  ovmpoga  6075  caovimo  6140  ofeq  6161  ofrval  6169  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  frecsuclem  6492  frecrdg  6494  domssr  6869  mapxpen  6945  diffifi  6991  unsnfidcex  7017  unsnfidcel  7018  unfidisj  7019  undifdc  7021  ssfidc  7034  iunfidisj  7048  sbthlemi9  7067  elfir  7075  djuassen  7329  dftap2  7363  mulcanenq  7498  ltanqg  7513  addnnnq0  7562  distrlem4prl  7697  distrlem4pru  7698  distrprg  7701  aptipr  7754  addsrpr  7858  mulsrpr  7859  mulasssrg  7871  ltpsrprg  7916  axmulass  7986  axpre-ltadd  7999  mul31  8203  addsubass  8282  subcan2  8297  subsub2  8300  subsub4  8305  npncan3  8310  pnpcan  8311  pnncan  8313  subcan  8327  subdi  8457  ltadd1  8502  leadd1  8503  leadd2  8504  ltsubadd  8505  lesubadd  8507  ltaddsub  8509  leaddsub  8511  lesub1  8529  lesub2  8530  ltsub1  8531  ltsub2  8532  ltaddsublt  8644  gt0add  8646  apreap  8660  lemul1  8666  reapmul1lem  8667  reapmul1  8668  reapadd1  8669  remulext1  8672  remulext2  8673  apadd2  8682  mulext2  8686  mulap0r  8688  leltap  8698  ltap  8706  apsub1  8715  recexaplem2  8725  mulcanap  8738  mulcanap2  8739  divvalap  8747  divcanap2  8753  diveqap0  8755  divrecap  8761  divrecap2  8762  divdirap  8770  divcanap3  8771  div11ap  8773  muldivdirap  8780  divcanap5  8787  redivclap  8804  div2negap  8808  apmul1  8861  apmul2  8862  div2subap  8910  ltdiv1  8941  ltmuldiv  8947  lemuldiv  8954  lt2msq1  8958  ltdiv23  8965  lediv23  8966  squeeze0  8977  ofnegsub  9035  difgtsumgt  9442  gtndiv  9468  eluz2  9654  eluzsub  9678  peano2uz  9704  nn01to3  9738  divge1  9845  ledivge1le  9848  addlelt  9890  xaddass  9991  xleadd1  9997  xltadd1  9998  ixxssixx  10024  lbico1  10052  lbicc2  10106  icoshftf1o  10113  fzen  10165  fzrev3  10209  fzrevral2  10228  nelfzo  10274  elfzo0  10306  elfzo0z  10308  fzosplitprm1  10363  qbtwnre  10399  flqwordi  10431  flqword2  10432  adddivflid  10435  flltdivnn0lt  10447  modqcl  10471  mulqmod0  10475  modqmulnn  10487  modqabs2  10503  addmodid  10517  modifeq2int  10531  modqeqmodmin  10539  seqeq2  10596  seqeq3  10597  seq1g  10608  seqp1g  10611  exp3val  10686  expnegap0  10692  expgt1  10722  exprecap  10725  leexp2a  10737  expubnd  10741  sqdivap  10748  expnbnd  10808  mulsubdivbinom2ap  10856  bccmpl  10899  fihashss  10961  leisorel  10982  ccatass  11064  ccats1val2  11092  swrdval  11101  swrdval2  11104  swrdlen2  11115  swrdfv2  11116  shftfibg  11131  mulreap  11175  abssubne0  11402  maxleast  11524  lemininf  11545  ltmininf  11546  xrmaxltsup  11569  xrmaxaddlem  11571  xrmaxadd  11572  xrmineqinf  11580  xrltmininf  11581  xrminltinf  11583  xrminadd  11586  climuni  11604  reccn2ap  11624  isumz  11700  fsumsplitsnun  11730  geoisum1c  11831  prod1dc  11897  efltim  12009  dvdscmulr  12131  dvdsmulcr  12132  summodnegmod  12133  modmulconst  12134  dvdsmultr2  12144  dvdsexp  12172  mulmoddvds  12174  modremain  12240  divgcdz  12292  gcdaddm  12305  dvdsgcdb  12334  gcdass  12336  mulgcd  12337  gcddiv  12340  rplpwr  12348  uzwodc  12358  lcmdvdsb  12406  lcmass  12407  mulgcddvds  12416  qredeq  12418  qredeu  12419  rpmul  12420  divgcdcoprmex  12424  cncongr1  12425  rpexp  12475  rpexp12i  12477  odzcllem  12565  odzdvds  12568  odzphi  12569  pythagtriplem15  12601  pcpremul  12616  pcdiv  12625  pcqmul  12626  pcqdiv  12630  dvdsprmpweq  12658  sumhashdc  12670  pcfaclem  12672  qexpz  12675  ctinf  12801  setsvala  12863  ressressg  12907  ressabsg  12908  rngbaseg  12968  ptex  13096  issubmnd  13274  ress0g  13275  imasmnd2  13284  gsumfzz  13327  grpasscan2  13396  grpidrcan  13397  grpidlcan  13398  grpinvadd  13410  grpsubeq0  13418  grppncan  13423  dfgrp3m  13431  grpsubpropd2  13437  pwsinvg  13444  imasgrp2  13446  mhmmnd  13452  mulgnegneg  13477  mulgaddcomlem  13481  mulgaddcom  13482  mulginvcom  13483  mulgmodid  13497  issubg  13509  nsgconj  13542  nsgid  13551  quselbasg  13566  quseccl0g  13567  ghmnsgima  13604  cmn4  13641  ablinvadd  13646  ablsub4  13649  abladdsub4  13650  ablpncan2  13652  rngpropd  13717  imasrng  13718  issrg  13727  ringidss  13791  ringcom  13793  imasring  13826  unitmulcl  13875  unitmulclb  13876  dvrcl  13897  unitdvcl  13898  dvrcan1  13902  dvrcan3  13903  issubrng  13961  subrngpropd  13978  rrgeq0  14027  islmod  14053  lmodcom  14095  rmodislmodlem  14112  rmodislmod  14113  lss0cl  14131  lssvnegcl  14138  lssintclm  14146  lssincl  14147  lspss  14161  lspun  14164  lspsnvsi  14180  lsslsp  14191  rnglidlmmgm  14258  rnglidlmsgrp  14259  rnglidlrng  14260  qus2idrng  14287  qusmulrng  14294  2basgeng  14554  clsss  14590  ntrss  14591  ntrin  14596  neiss  14622  restco  14646  restabs  14647  lmconst  14688  psmetsym  14801  psmetge0  14803  xmetge0  14837  xmetsym  14840  xmetresbl  14912  mopni3  14956  bdxmet  14973  bdmopn  14976  txmetcnp  14990  dvfvalap  15153  dvid  15167  dvidre  15169  dvcnp2cntop  15171  elplyr  15212  ply1term  15215  ptolemy  15296  rpcxpadd  15377  rpmulcxp  15381  rpdivcxp  15383  cxpmul  15384  rpcxple2  15390  rpcxplt2  15391  cxpcom  15410  rplogbval  15417  rplogbcl  15418  rprelogbmulexp  15428  relogbexpap  15430  logbleb  15433  logblt  15434  rplogbcxp  15435  rpcxplogb  15436  sgmppw  15464  lgslem1  15477  lgsfcl2  15483  lgsneg  15501  lgsne0  15515  lgssq2  15518  lgsdirnn0  15524  gausslemma2dlem1a  15535  lgsquad  15557  2lgsoddprmlem2  15583  funvtxvalg  15633  funiedgvalg  15634