Theorem simprr 451

Description: Simplification of a conjunction.

Assertion

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

Proof of Theorem simprr

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  simp1rr 942  simp2rr 946  simp3rr 950  reuuniss2 3817  1stconst 5070  2ndconst 5071  reiotass2 5111  sdomdomtr 5532  ordiso 5683  hartoglem 5692  omsublim 5887  omsubinit 5890  mulgt0sr 6366  muladdOLD 6583  divdivdiv 6961  lemul2aOLD 7022  ltmul12a 7023  lemulge11 7030  lt2mul2div 7054  lediv12a 7079  modadd1 7518  modmul1 7519  elfzle2 7654  elfz2nn0 7667  fzrev 7689  exprecOLD 7838  le2sq2 7877  bernneq 7898  bernneqOLD 7899  fsumdivc 8295  fsumdivcALT 8296  fsum0diaglem2 8519  tgval3 8895  tgss2 8907  ssnei2 9006  cnpcl 9040  cnco 9045  cncnplem1 9051  cnconst 9057  blcntr 9122  blelrn 9125  blss 9130  opnuni 9145  metcnplem 9164  lmle 9238  xplmi 9251  lmcau 9274  bcthlem11 9287  grpidinvlem2 9329  grpinvid1 9356  grpinvid2 9357  grplcan 9359  ssga 9455  gapmlem 9461  ringideu 9470  nvsubadd 9607  nvnpcan 9612  nvmeq0 9616  nvabs 9633  vacnlem6 9672  lnomul 9760  psasym 9994  oprabopabf 10157  fipreima 10175  subtopmetlem 10255  subtopmet 10256  fbunfip 10282  elfilmap 10312  elfilmap2 10313  elfilmap3 10314  tosdir 10358  ismnd1 10391  rnplrnml 10404  5oalem5 11238  unoplin 11481  hmoplin 11503  bralnfn 11509  hmops 11582  hmopm 11583  hmopco 11585  adjadd 11663  kbass3 11689  strlem3a 11824  csmdsymi 11906  ghomf1olem 13637  axfelem15 14045  cljo 14534  clme 14535  valcurfn1 14552  definc 14621  domncnt 14624  ranncnt 14625  toplat 14638  dfdir2 14639  resgcom 14712  fprodadd 14713  curgrpact 14735  fprodsub 14742  sub2vec 14815  mvecrtol 14816  prtoptop 14919  altretop 14997  trnij 15015  finminlem 15367  elfiun 15369  finsschain 15373  ordisoOLD 15374  hartoglemOLD 15383  omsublimOLD 15396  omsubinitOLD 15399  cnntr 15420  subntr 15425  cnsubsp2 15427  compsub 15431  uncomp 15433  compfipin0lem 15435  compfipin0 15436  alexsublem2 15438  reconnlem5 15450  ivthALT 15454  2ndcsb 15476  2ndc1stc 15477  2ndcctbss 15478  isfne3 15482  fneint 15486  fnetr 15495  topfneec 15501  fnessref 15503  lfinpfin 15513  comppfsc 15517  neibastop2lem1 15519  neibastop2lem2 15520  fnemeet2 15529  fnejoin1 15530  isufil2 15565  filssufillem 15570  ufileu 15573  filufint 15574  ufinffr 15578  ufilen 15579  limfilcf 15587  cnpfillim 15589  rnelfm 15593  fmfnfmlem1 15594  fmfnfmlem2 15595  fmfnfmlem4 15597  flimfbas 15601  fcluscf 15612  flimfnfcls 15615  fcluscnp 15618  fcluscomplem 15620  filnetlem4 15643  filnetlem5 15644  filnet 15645  fipreimaOLD 15756  cnres 15889  txsubsp 15912  sstotbnd 15936  totbndbnd 15944  ismtyhmeolem 15950  heiborlem18 15972  rrntotbndlem2 16021  rrntotbnd 16022  ghomdiv 16041  phtpyco 16056  phtpcer 16062  pcohtpy 16083  pi1gp 16095  hlhght4 17037  cvr1 17054  grpidinvlem2NEW 17110  grpinvid1NEW 17131  grpinvid2NEW 17132  grplcanNEW 17134  isline2 17248  paddcom 17274  paddasslem4 17284  paddasslem6 17286  paddasslem7 17287  pmodl42 17312  pmapjoin 17313  poml4 17361  osumcllem4 17367  pexmidlem1 17378  pexmidlem3 17380  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