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  3590  ifeq2da  3591  ifclda  3592  ifbothda  3595  posn  4758  frsn  4760  somin1  5079  somincom  5080  xpcan  5112  fvmpti  5601  fvmptss  5609  funressn  5706  riotassuni  6343  oeoa  6595  oeoe  6597  omabs  6645  eceqoveq  6763  domdifsn  6945  pw2f1olem  6966  mapdom1  7026  marypha1lem  7186  infdifsn  7357  carden2b  7600  fidomtri  7626  dfac12lem2  7770  cdadom1  7812  infunsdom1  7839  infunsdom  7840  itunisuc  8045  gchdomtri  8251  xrmax2  10505  xrmin1  10506  ifle  10524  xmulneg1  10589  xrsupsslem  10625  xrinfmsslem  10626  fzneuz  10863  seqf1olem1  11085  bccmpl  11322  bcval5  11330  bcpasc  11333  bccl  11334  hasheni  11347  hashfn  11357  hashdom  11361  hashdomi  11362  hashbc  11391  sumz  12195  sumss  12197  sumsplit  12231  bitsmod  12627  sadadd2lem2  12641  sadcaddlem  12648  gcddvds  12694  gcdcl  12696  gcdneg  12705  pcgcd  12930  pcmpt  12940  pcmpt2  12941  pcprod  12943  fldivp1  12945  prmreclem4  12966  vdwlem6  13033  ramub1lem1  13073  cidpropd  13613  rescabs  13710  acsexdimd  14286  gsumval2  14460  gsumval3  15191  ablfac1c  15306  ablfac1eu  15308  mgpress  15336  psrbas  16124  resspsrbas  16159  mplmonmul  16208  mplcoe1  16209  mplcoe2  16211  opsrle  16217  opsrbaslem  16219  psrbaspropd  16312  mplbaspropd  16314  opnnei  16857  restbas  16889  hauspwdom  17227  ptcmplem5  17750  xrsmopn  18318  xrhmeo  18444  lebnum  18462  pcohtpylem  18517  pcoass  18522  pcorevlem  18524  icombl  18921  ioombl  18922  mbfconstlem  18984  mbfima  18987  i1fd  19036  mbfi1fseqlem5  19074  itg2const2  19096  itg2seq  19097  itg2uba  19098  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  iblss  19159  iblss2  19160  itgss  19166  bddmulibl  19193  coemullem  19631  aaliou2b  19721  isppw2  20353  mule1  20386  ppip1le  20399  dchrelbas3  20477  dchrpt  20506  bposlem3  20525  bposlem5  20527  bposlem6  20528  lgslem4  20538  lgsneg  20558  lgsmod  20560  lgsdilem  20561  lgsdir  20569  lgsdi  20571  lgsne0  20572  lgsquad3  20600  dchrvmasum2if  20646  nmcfnlbi  22632  xrge0npcan  23333  disjdifprg  23352  gsumpropd2lem  23379  esumcvg  23454  erdsze2lem1  23734  trpredlem1  24230  areacirclem6  24930  ttac  27129  pw2f1ocnv  27130  aomclem5  27155  frlmsslsp  27248  isnumbasgrplem3  27270  f1otrspeq  27390  pmtrfinv  27402  psgnunilem1  27416  fnchoice  27700  fmul01lt1lem1  27714  fmul01lt1lem2  27715  stoweidlem14  27763  stoweidlem26  27775  stoweidlem28  27777  stoweidlem55  27804  stoweidlem58  27807  stoweid  27812  stirlinglem5  27827  stirlinglem12  27834  sharhght  27855  3dim1  29656  3dim2  29657  3dim3  29658  3atlem3  29674  3atlem7  29678  lvolnle3at  29771  2lplnja  29808  paddasslem18  30026  lhpexle3lem  30200  4atex  30265  cdlemd5  30391  cdleme16  30474  cdleme20  30513  cdleme21j  30525  cdleme21  30526  cdleme32snaw  30624  cdleme32fvcl  30629  cdleme32le  30636  cdlemeg46gf  30722  cdleme48gfv  30726  cdleme50trn12  30741  cdlemg6  30812  cdlemg7N  30815  cdlemg38  30904  cdlemg46  30924  dibvalrel  31353  dihlss  31440  dihglblem5aN  31482  dihmeetbN  31493  dihmeetALTN  31517  dihatlat  31524  dihatexv  31528  dvh3dim2  31638  dvh3dim3N  31639  lclkrlem2h  31704  mapdh8d  31973  mapdh8g  31976  hdmap11lem2  32035
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