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

Theorem pm2.61dan 782
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 434 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61dan.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  ch )
43ex 434 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
52, 4pm2.61d 158 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  pm2.61ddan  783  pm2.61dda  784  nfsb4t  2078  ifeq1da  3807  ifeq2da  3808  ifclda  3809  ifeqda  3810  ifbothda  3812  2if2  3825  posn  4894  frsn  4896  somin1  5222  somincom  5223  xpcan  5262  fvmpti  5761  fvmptss  5770  funressn  5882  ovima0  6231  oeoa  7024  oeoe  7026  omabs  7074  eceqoveq  7193  domdifsn  7382  pw2f1olem  7403  mapdom1  7464  marypha1lem  7671  supval2  7693  infdifsn  7850  carden2b  8125  fidomtri  8151  dfac12lem2  8301  cdadom1  8343  infunsdom1  8370  infunsdom  8371  itunisuc  8576  gchdomtri  8784  xrmax2  11136  xrmin1  11137  ifle  11155  xmulneg1  11220  xrsupsslem  11257  xrinfmsslem  11258  fzneuz  11525  seqf1olem1  11829  bccmpl  12069  bcval5  12078  bcpasc  12081  bccl  12082  hasheni  12103  hashfn  12122  hashdom  12126  hashdomi  12127  hashge1  12136  hashbc  12190  sumz  13183  sumss  13185  sumsplit  13219  bitsmod  13615  sadadd2lem2  13629  sadcaddlem  13636  gcddvds  13682  gcdcl  13684  gcdneg  13693  pcgcd  13927  pcmpt  13937  pcmpt2  13938  pcprod  13940  fldivp1  13942  prmreclem4  13963  vdwlem6  14030  ramub1lem1  14070  cidpropd  14632  rescabs  14729  lubval  15137  glbval  15150  joinval  15158  meetval  15172  acsexdimd  15336  gsumval2  15493  f1otrspeq  15933  pmtrfinv  15947  psgnunilem1  15979  gsumval3OLD  16362  gsumval3  16365  ablfac1c  16546  ablfac1eu  16548  mgpress  16576  psrbas  17382  psrbasOLD  17383  resspsrbas  17421  mplmonmul  17477  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  opsrle  17489  opsrbaslem  17491  psrbaspropd  17587  mplbaspropd  17589  frlmsslsp  18065  frlmsslspOLD  18066  mdet1  18250  mdetunilem7  18266  mdetunilem9  18268  maducoeval2  18288  madurid  18292  opnnei  18566  restbas  18604  hauspwdom  18947  ptcmplem5  19470  xrsmopn  20231  xrhmeo  20360  lebnum  20378  pcohtpylem  20433  pcoass  20438  pcorevlem  20440  icombl  20887  ioombl  20888  mbfconstlem  20949  mbfima  20952  i1fd  21001  mbfi1fseqlem5  21039  itg2const2  21061  itg2seq  21062  itg2uba  21063  itg2splitlem  21068  itg2split  21069  itg2monolem1  21070  itg2gt0  21080  itg2cnlem1  21081  itg2cnlem2  21082  iblss  21124  iblss2  21125  itgss  21131  bddmulibl  21158  coemullem  21602  aaliou2b  21692  isppw2  22338  mule1  22371  ppip1le  22384  dchrelbas3  22462  dchrpt  22491  bposlem3  22510  bposlem5  22512  bposlem6  22513  lgslem4  22523  lgsneg  22543  lgsmod  22545  lgsdilem  22546  lgsdir  22554  lgsdi  22556  lgsne0  22557  lgsquad3  22585  dchrvmasum2if  22631  nmcfnlbi  25279  elpreq  25724  disjdifprg  25743  xrge0npcan  25981  archiabl  26039  gsumpropd2lem  26093  orngsqr  26125  esumcst  26368  hasheuni  26388  esumcvg  26389  ddemeas  26506  eulerpartlemgc  26593  eulerpartlemb  26599  plymulx  26797  signswmnd  26806  erdsze2lem1  26939  prod1  27304  prodss  27307  trpredlem1  27538  wl-cbvalnaed  28209  wl-nfeqfb  28214  itg2addnclem  28287  itg2addnclem2  28288  iblmulc2nc  28301  ftc1anclem5  28315  ftc1anc  28319  dvasin  28324  areacirclem5  28332  exmid2  28746  ttac  29230  pw2f1ocnv  29231  aomclem5  29256  isnumbasgrplem3  29306  iocmbl  29433  fnchoice  29596  fmul01lt1lem1  29610  fmul01lt1lem2  29611  stoweidlem14  29655  stoweidlem26  29667  stoweidlem28  29669  stoweidlem55  29696  stoweid  29704  stirlinglem5  29719  stirlinglem12  29726  sharhght  29747  3dim1  32684  3dim2  32685  3dim3  32686  3atlem3  32702  3atlem7  32706  lvolnle3at  32799  2lplnja  32836  paddasslem18  33054  lhpexle3lem  33228  4atex  33293  cdlemd5  33419  cdleme16  33502  cdleme20  33541  cdleme21j  33553  cdleme21  33554  cdleme32snaw  33652  cdleme32fvcl  33657  cdleme32le  33664  cdlemeg46gf  33750  cdleme48gfv  33754  cdleme50trn12  33769  cdlemg6  33840  cdlemg7N  33843  cdlemg38  33932  cdlemg46  33952  dibvalrel  34381  dihlss  34468  dihglblem5aN  34510  dihmeetbN  34521  dihmeetALTN  34545  dihatlat  34552  dihatexv  34556  dvh3dim2  34666  dvh3dim3N  34667  lclkrlem2h  34732  mapdh8d  35001  mapdh8g  35004  hdmap11lem2  35063
  Copyright terms: Public domain W3C validator