MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61dan Unicode version

Theorem pm2.61dan 766
Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
pm2.61dan.1  |-  ( (
ph  /\  ps )  ->  ch )
pm2.61dan.2  |-  ( (
ph  /\  -.  ps )  ->  ch )
Assertion
Ref Expression
pm2.61dan  |-  ( ph  ->  ch )

Proof of Theorem pm2.61dan
StepHypRef Expression
1 pm2.61dan.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 423 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61dan.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  ch )
43ex 423 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
52, 4pm2.61d 150 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358
This theorem is referenced by:  pm2.61ddan  767  pm2.61dda  768  ifeq1da  3666  ifeq2da  3667  ifclda  3668  ifbothda  3671  posn  4837  frsn  4839  somin1  5158  somincom  5159  xpcan  5191  fvmpti  5681  fvmptss  5689  funressn  5787  riotassuni  6427  oeoa  6679  oeoe  6681  omabs  6729  eceqoveq  6848  domdifsn  7030  pw2f1olem  7051  mapdom1  7111  marypha1lem  7273  infdifsn  7444  carden2b  7687  fidomtri  7713  dfac12lem2  7857  cdadom1  7899  infunsdom1  7926  infunsdom  7927  itunisuc  8132  gchdomtri  8338  xrmax2  10594  xrmin1  10595  ifle  10613  xmulneg1  10678  xrsupsslem  10714  xrinfmsslem  10715  fzneuz  10952  seqf1olem1  11174  bccmpl  11412  bcval5  11420  bcpasc  11423  bccl  11424  hasheni  11437  hashfn  11447  hashdom  11451  hashdomi  11452  hashbc  11481  sumz  12286  sumss  12288  sumsplit  12322  bitsmod  12718  sadadd2lem2  12732  sadcaddlem  12739  gcddvds  12785  gcdcl  12787  gcdneg  12796  pcgcd  13021  pcmpt  13031  pcmpt2  13032  pcprod  13034  fldivp1  13036  prmreclem4  13057  vdwlem6  13124  ramub1lem1  13164  cidpropd  13706  rescabs  13803  acsexdimd  14379  gsumval2  14553  gsumval3  15284  ablfac1c  15399  ablfac1eu  15401  mgpress  15429  psrbas  16217  resspsrbas  16252  mplmonmul  16301  mplcoe1  16302  mplcoe2  16304  opsrle  16310  opsrbaslem  16312  psrbaspropd  16405  mplbaspropd  16407  opnnei  16957  restbas  16989  hauspwdom  17327  ptcmplem5  17846  xrsmopn  18414  xrhmeo  18542  lebnum  18560  pcohtpylem  18615  pcoass  18620  pcorevlem  18622  icombl  19019  ioombl  19020  mbfconstlem  19082  mbfima  19085  i1fd  19134  mbfi1fseqlem5  19172  itg2const2  19194  itg2seq  19195  itg2uba  19196  itg2splitlem  19201  itg2split  19202  itg2monolem1  19203  itg2gt0  19213  itg2cnlem1  19214  itg2cnlem2  19215  iblss  19257  iblss2  19258  itgss  19264  bddmulibl  19291  coemullem  19729  aaliou2b  19819  isppw2  20459  mule1  20492  ppip1le  20505  dchrelbas3  20583  dchrpt  20612  bposlem3  20631  bposlem5  20633  bposlem6  20634  lgslem4  20644  lgsneg  20664  lgsmod  20666  lgsdilem  20667  lgsdir  20675  lgsdi  20677  lgsne0  20678  lgsquad3  20706  dchrvmasum2if  20752  nmcfnlbi  22740  disjdifprg  23213  xrge0npcan  23408  gsumpropd2lem  23412  esumcvg  23742  erdsze2lem1  24138  prod1  24571  prodss  24574  trpredlem1  24788  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  iblmulc2nc  25505  areacirclem6  25522  ttac  26452  pw2f1ocnv  26453  aomclem5  26478  frlmsslsp  26571  isnumbasgrplem3  26593  f1otrspeq  26713  pmtrfinv  26725  psgnunilem1  26739  fnchoice  27023  fmul01lt1lem1  27037  fmul01lt1lem2  27038  stoweidlem14  27086  stoweidlem26  27098  stoweidlem28  27100  stoweidlem55  27127  stoweidlem58  27130  stoweid  27135  stirlinglem5  27150  stirlinglem12  27157  sharhght  27178  3dim1  29708  3dim2  29709  3dim3  29710  3atlem3  29726  3atlem7  29730  lvolnle3at  29823  2lplnja  29860  paddasslem18  30078  lhpexle3lem  30252  4atex  30317  cdlemd5  30443  cdleme16  30526  cdleme20  30565  cdleme21j  30577  cdleme21  30578  cdleme32snaw  30676  cdleme32fvcl  30681  cdleme32le  30688  cdlemeg46gf  30774  cdleme48gfv  30778  cdleme50trn12  30793  cdlemg6  30864  cdlemg7N  30867  cdlemg38  30956  cdlemg46  30976  dibvalrel  31405  dihlss  31492  dihglblem5aN  31534  dihmeetbN  31545  dihmeetALTN  31569  dihatlat  31576  dihatexv  31580  dvh3dim2  31690  dvh3dim3N  31691  lclkrlem2h  31756  mapdh8d  32025  mapdh8g  32028  hdmap11lem2  32087
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator