Theorem simpll 412

Description: Simplification of a conjunction.

Assertion

Ref	Expression
simpll	|- (((ph /\ ps) /\ ch) -> ph)

Proof of Theorem simpll

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ph -> ph)
2	1	ad2antrr 404	1 |- (((ph /\ ps) /\ ch) -> ph)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sspr 2475  ordelord 2970  oaass 4195  ltexpq 5080  prn0 5093  cnegextlem1 5345  cnegext 5348  conjmult 5797  ltmul12it 5841  lemul12it 5844  lemulge11t 5848  zltp1let 6181  elfzel1 6481  elfz2nn0t 6495  fzrevt 6511  expaddt 6596  expmult 6597  expmwordit 6606  expnlbndt 6655  cvg2 6922  caubnd 6926  bcclt 6972  fsumsplit 7020  fsumcom 7028  fsumdivc 7035  fsumdivcALT 7036  climsub 7130  climsqueeze 7140  climsqueeze2 7141  climcau 7156  caucvg 7163  cvgcmp3c 7186  isum1p 7206  reccnv 7218  cvgratlem1 7250  efaddlem23 7360  acdc3lem 7486  acdc2lem1 7488  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  infdif 7568  tgss2t 7637  neissex 7738  clslp 7748  dnsconst 7788  ssblex 7856  opnuni 7868  lpbl 7880  metcnplem 7886  tgioolem 7914  lmbr 7928  lmle 7960  xplm 7975  lmcau 7996  cmsss 7997  bcthlem16 8014  bcthlem30 8028  grpidinvlem4 8051  grpideu 8053  grpidinv2 8060  grplid 8061  abl4 8105  blocnilem 8464  ubthlem5 8533  spwpr4OLD 8663  spwpr4aOLD 8664  hvmul0ort 8894  shex 9077  3oalem2 9608  bralnfnt 9872  kbpjt 9880  eighmortht 9888  hmopmt 9946  hmopcot 9948  lnopcon 9963  lnfncon 9990  riesz3 9995  cnlnadjlem6 10005  adjmult 10025  kbass5t 10053  leopmulit 10066  nmopleidt 10072  dmdbr2 10230  mdslmd1lem1 10252  superpos 10281  irredlem2 10318  irred 10321  atcvat4 10324  cdrci 10494  qusp 10555  sfvlim 10605  iintlem1 10632  icmpmon 10744  idmon 10745

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain