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

Theorem pm2.61dan 789
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  790  pm2.61dda  791  nfsb4t  2114  ifeq1da  3952  ifeq2da  3953  ifclda  3954  ifeqda  3955  ifbothda  3957  2if2  3970  posn  5054  frsn  5056  somin1  5389  xpcan  5429  fvmpti  5936  fvmptss  5945  funressn  6065  ovima0  6435  oeoa  7244  oeoe  7246  omabs  7294  eceqoveq  7414  domdifsn  7598  pw2f1olem  7619  mapdom1  7680  marypha1lem  7891  supval2  7913  infdifsn  8071  carden2b  8346  fidomtri  8372  dfac12lem2  8522  cdadom1  8564  infunsdom1  8591  infunsdom  8592  itunisuc  8797  gchdomtri  9005  xrmax2  11381  xrmin1  11382  ifle  11400  xmulneg1  11465  xrsupsslem  11502  xrinfmsslem  11503  fzneuz  11763  seqf1olem1  12120  bccmpl  12361  bcval5  12370  bcpasc  12373  bccl  12374  hasheni  12395  hashfn  12417  hashdom  12421  hashdomi  12422  hashge1  12431  hashbc  12476  sumz  13518  sumss  13520  sumsplit  13557  bitsmod  13958  sadadd2lem2  13972  sadcaddlem  13979  gcddvds  14025  gcdcl  14027  gcdneg  14036  pcgcd  14273  pcmpt  14283  pcmpt2  14284  pcprod  14286  fldivp1  14288  prmreclem4  14309  vdwlem6  14376  ramub1lem1  14416  cidpropd  14977  rescabs  15074  lubval  15483  glbval  15496  joinval  15504  meetval  15518  acsexdimd  15682  gsumpropd2lem  15769  gsumval2  15776  f1otrspeq  16341  pmtrfinv  16355  psgnunilem1  16387  gsumval3OLD  16777  gsumval3  16780  ablfac1c  16990  ablfac1eu  16992  mgpress  17020  psrbas  17898  psrbasOLD  17899  resspsrbas  17938  mplmonmul  17994  mplcoe1  17995  mplcoe5  17999  mplcoe2OLD  18001  opsrle  18008  opsrbaslem  18010  psrbaspropd  18144  mplbaspropd  18146  frlmsslsp  18696  frlmsslspOLD  18697  mdetdiag  18968  mdetunilem7  18987  mdetunilem9  18989  maducoeval2  19009  madurid  19013  opnnei  19487  restbas  19525  hauspwdom  19868  ptcmplem5  20422  xrsmopn  21183  xrhmeo  21312  lebnum  21330  pcohtpylem  21385  pcoass  21390  pcorevlem  21392  icombl  21840  ioombl  21841  mbfconstlem  21902  mbfima  21905  i1fd  21954  mbfi1fseqlem5  21992  itg2const2  22014  itg2seq  22015  itg2uba  22016  itg2splitlem  22021  itg2split  22022  itg2monolem1  22023  itg2gt0  22033  itg2cnlem1  22034  itg2cnlem2  22035  iblss  22077  iblss2  22078  itgss  22084  bddmulibl  22111  coemullem  22512  aaliou2b  22602  isppw2  23254  mule1  23287  ppip1le  23300  dchrelbas3  23378  dchrpt  23407  bposlem3  23426  bposlem5  23428  bposlem6  23429  lgslem4  23439  lgsneg  23459  lgsmod  23461  lgsdilem  23462  lgsdir  23470  lgsdi  23472  lgsne0  23473  lgsquad3  23501  dchrvmasum2if  23547  midexlem  23934  colperpex  23972  lnopp2hpgb  23997  lmieu  24015  nmcfnlbi  26836  elpreq  27282  disjdifprg  27301  xrge0npcan  27550  archiabl  27608  orngsqr  27660  esumcst  27937  hasheuni  27957  esumcvg  27958  ddemeas  28074  eulerpartlemgc  28167  eulerpartlemb  28173  plymulx  28371  signswmnd  28380  signstfvneq0  28395  erdsze2lem1  28513  mrsubvrs  28748  prod1  29044  prodss  29047  trpredlem1  29278  wl-cbvalnaed  29953  wl-nfeqfb  29958  itg2addnclem  30034  itg2addnclem2  30035  iblmulc2nc  30048  ftc1anclem5  30062  ftc1anc  30066  dvasin  30071  areacirclem5  30079  exmid2  30467  ttac  30946  pw2f1ocnv  30947  aomclem5  30972  isnumbasgrplem3  31022  iocmbl  31149  radcnvrat  31164  dvdslcm  31173  lcmcl  31176  lcmneg  31178  lcmgcd  31182  fnchoice  31351  fzisoeu  31445  fperiodmul  31449  upbdrech2  31453  ioondisj2  31457  iccdifprioo  31488  fmul01lt1lem1  31502  fmul01lt1lem2  31503  limciccioolb  31531  lptioo2  31541  lptioo1  31542  limcicciooub  31547  lptre2pt  31550  limcresiooub  31552  limcresioolb  31553  limcleqr  31554  coskpi2  31569  cosknegpi  31572  icccncfext  31593  cncfiooicclem1  31599  cncfiooicc  31600  cncfiooiccre  31601  dvbdfbdioolem2  31626  ioodvbdlimc1lem1  31628  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  volioc  31657  itgioocnicc  31662  iblcncfioo  31663  stoweidlem14  31681  stoweidlem26  31693  stoweidlem28  31695  stoweidlem55  31722  stoweid  31730  stirlinglem5  31745  stirlinglem12  31752  dirkerper  31763  dirkertrigeqlem3  31767  dirkertrigeq  31768  dirkercncflem1  31770  dirkercncflem2  31771  dirkercncf  31774  fourierdlem10  31784  fourierdlem12  31786  fourierdlem24  31798  fourierdlem30  31804  fourierdlem31  31805  fourierdlem32  31806  fourierdlem33  31807  fourierdlem34  31808  fourierdlem35  31809  fourierdlem37  31811  fourierdlem40  31814  fourierdlem41  31815  fourierdlem42  31816  fourierdlem43  31817  fourierdlem44  31818  fourierdlem46  31820  fourierdlem48  31822  fourierdlem49  31823  fourierdlem51  31825  fourierdlem54  31828  fourierdlem62  31836  fourierdlem64  31838  fourierdlem65  31839  fourierdlem70  31844  fourierdlem71  31845  fourierdlem73  31847  fourierdlem74  31848  fourierdlem75  31849  fourierdlem78  31852  fourierdlem79  31853  fourierdlem80  31854  fourierdlem81  31855  fourierdlem82  31856  fourierdlem92  31866  fourierdlem93  31867  fourierdlem97  31871  fourierdlem101  31875  fourierdlem102  31876  fourierdlem103  31877  fourierdlem104  31878  fourierdlem109  31883  fourierdlem114  31888  sqwvfoura  31896  sqwvfourb  31897  fourierswlem  31898  fouriersw  31899  sharhght  31916  3dim1  34893  3dim2  34894  3dim3  34895  3atlem3  34911  3atlem7  34915  lvolnle3at  35008  2lplnja  35045  paddasslem18  35263  lhpexle3lem  35437  4atex  35502  cdlemd5  35629  cdleme16  35712  cdleme20  35752  cdleme21j  35764  cdleme21  35765  cdleme32snaw  35863  cdleme32fvcl  35868  cdleme32le  35875  cdlemeg46gf  35961  cdleme48gfv  35965  cdleme50trn12  35980  cdlemg6  36051  cdlemg7N  36054  cdlemg38  36143  cdlemg46  36163  dibvalrel  36592  dihlss  36679  dihglblem5aN  36721  dihmeetbN  36732  dihmeetALTN  36756  dihatlat  36763  dihatexv  36767  dvh3dim2  36877  dvh3dim3N  36878  lclkrlem2h  36943  mapdh8d  37212  mapdh8g  37215  hdmap11lem2  37274
  Copyright terms: Public domain W3C validator