Theorem simpll 448

Description: Simplification of a conjunction.

Assertion

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

Proof of Theorem simpll

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  simp1ll 939  simp2ll 943  simp3ll 947  sspr 3144  ordelord 3680  oaass 5243  riota5 5580  ordtypelem6 5689  ordtypelem7 5690  omsubinit 5890  ltexpq 6232  prn0 6245  cnegexlem1 6499  cnegex 6502  divdivdiv 6961  divdivdivOLD 6962  conjmul 6975  ltmul12a 7023  lemul12a 7026  lemulge11 7030  lt2mul2div 7054  zltp1le 7390  qreccl 7453  modid 7512  elfzel1 7651  elfz2nn0 7667  fzrev 7689  expadd 7839  expmul 7840  expmwordi 7851  expnlbnd 7902  expnlbnd2 7903  digit1 7905  cvg2i 8174  caubndi 8178  bccl 8224  fsumsplit 8280  fsumcom 8288  fsumdivc 8295  fsumdivcALT 8296  climsub 8390  climsqueeze 8400  climsqueeze2 8401  climcaui 8416  caucvgi 8423  cvgcmp3ci 8447  isum1p 8467  reccnv 8479  cvgratlem1 8512  efaddlem23 8622  acdc3lem 8754  acdc2lem1 8757  acdc2lem2 8758  acdc5lem2 8761  acdclem 8763  infdif 8837  tgss2 8907  neissex 9014  clslp 9024  cnpnei 9043  dnsconst 9065  opnuni 9145  lpbl 9157  metcnplem 9164  tgioolem 9192  lmbr 9206  lmle 9238  xplm 9253  lmcau 9274  cmsss 9275  bcthlem16 9292  bcthlem30 9306  grpidinvlem4 9331  grpideu 9333  grpidinv2 9344  grplid 9345  ssga 9455  vacnlem3 9669  blocnilem 9804  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  cdrci 10182  txcn 10227  elsubsp 10248  subcld 10254  subtopmet 10256  fbssint 10279  sfvlim 10296  hausfillim 10303  hvmul0or 10526  shex 10710  3oalem2 11243  bralnfn 11509  kbpj 11517  eighmorth 11525  hmopm 11583  hmopco 11585  lnopconi 11600  lnfnconi 11627  riesz3i 11632  cnlnadjlem6 11642  adjmul 11662  kbass5 11691  leopmuli 11704  nmopleid 11710  dmdbr2 11875  mdslmd1lem1 11897  superpos 11926  irredlem2 11963  irredi 11966  atcvat4i 11969  sltval2 13997  axdense 14027  axfelem16 14046  inpreima5 14469  npincppr 14501  geme2 14617  ranncnt 14625  dfdir2 14639  trran2 14757  osneisi 14875  qusp 14908  iintlem1 15010  flimfneicn 15037  dualded 15132  dualcat2 15133  icmpmon 15165  iepiclem 15172  elfiun 15369  finsschain 15373  ordtypelem6OLD 15380  ordtypelem7OLD 15381  omsubinitOLD 15399  cnsubsp 15426  compsub 15431  uncomp 15433  hscptsscld 15434  2ndcsb 15476  2ndcctbss 15478  topfneec 15501  fnessref 15503  refssfne 15504  comppfsc 15517  neibastop2lem2 15520  fnemeet2 15529  isufil2 15565  filssufillem 15570  uffixfr 15575  limfilcf 15587  rnelfm 15593  fmfnfmlem4 15597  fclsfnflim 15614  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  subspopn 15837  subspabs 15840  blssp 15844  mettrifi2 15848  icoopnst 15876  lincmb01cmp 15878  cnresima 15891  sstotbnd 15936  ismtyhmeolem 15950  heiborlem13 15967  heiborlem18 15972  heiborlem35 15989  rrndstprj1 16017  rrntotbndlem2 16021  iccbnd 16026  phtpycolem5 16055  phtpyco 16056  phtpcer 16062  reparpht 16065  pcohtpy 16083  pi1gp 16095  cvr1 17054  atcvrj2b 17069  atltcvr 17072  cvrat4 17076  grpidinvlem4NEW 17112  grpideuNEW 17114  grpidinv2NEW 17119  grplidNEW 17120  pmapglb2 17253  pmapglb2x 17254  pmodi 17309  osumcl 17375  pexmid 17377  pexmidlem8 17385

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 164  df-an 242

Copyright terms: Public domain