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  2096  ifeq1da  3962  ifeq2da  3963  ifclda  3964  ifeqda  3965  ifbothda  3967  2if2  3980  posn  5060  frsn  5062  somin1  5394  somincom  5395  xpcan  5434  fvmpti  5940  fvmptss  5949  funressn  6065  ovima0  6429  oeoa  7236  oeoe  7238  omabs  7286  eceqoveq  7406  domdifsn  7590  pw2f1olem  7611  mapdom1  7672  marypha1lem  7882  supval2  7904  infdifsn  8062  carden2b  8337  fidomtri  8363  dfac12lem2  8513  cdadom1  8555  infunsdom1  8582  infunsdom  8583  itunisuc  8788  gchdomtri  8996  xrmax2  11366  xrmin1  11367  ifle  11385  xmulneg1  11450  xrsupsslem  11487  xrinfmsslem  11488  fzneuz  11748  seqf1olem1  12102  bccmpl  12342  bcval5  12351  bcpasc  12354  bccl  12355  hasheni  12376  hashfn  12398  hashdom  12402  hashdomi  12403  hashge1  12412  hashbc  12455  sumz  13493  sumss  13495  sumsplit  13532  bitsmod  13934  sadadd2lem2  13948  sadcaddlem  13955  gcddvds  14001  gcdcl  14003  gcdneg  14012  pcgcd  14249  pcmpt  14259  pcmpt2  14260  pcprod  14262  fldivp1  14264  prmreclem4  14285  vdwlem6  14352  ramub1lem1  14392  cidpropd  14955  rescabs  15052  lubval  15460  glbval  15473  joinval  15481  meetval  15495  acsexdimd  15659  gsumpropd2lem  15811  gsumval2  15819  f1otrspeq  16261  pmtrfinv  16275  psgnunilem1  16307  gsumval3OLD  16692  gsumval3  16695  ablfac1c  16905  ablfac1eu  16907  mgpress  16935  psrbas  17794  psrbasOLD  17795  resspsrbas  17834  mplmonmul  17890  mplcoe1  17891  mplcoe5  17895  mplcoe2OLD  17897  opsrle  17904  opsrbaslem  17906  psrbaspropd  18040  mplbaspropd  18042  frlmsslsp  18589  frlmsslspOLD  18590  mdetdiag  18861  mdetunilem7  18880  mdetunilem9  18882  maducoeval2  18902  madurid  18906  opnnei  19380  restbas  19418  hauspwdom  19761  ptcmplem5  20284  xrsmopn  21045  xrhmeo  21174  lebnum  21192  pcohtpylem  21247  pcoass  21252  pcorevlem  21254  icombl  21702  ioombl  21703  mbfconstlem  21764  mbfima  21767  i1fd  21816  mbfi1fseqlem5  21854  itg2const2  21876  itg2seq  21877  itg2uba  21878  itg2splitlem  21883  itg2split  21884  itg2monolem1  21885  itg2gt0  21895  itg2cnlem1  21896  itg2cnlem2  21897  iblss  21939  iblss2  21940  itgss  21946  bddmulibl  21973  coemullem  22374  aaliou2b  22464  isppw2  23110  mule1  23143  ppip1le  23156  dchrelbas3  23234  dchrpt  23263  bposlem3  23282  bposlem5  23284  bposlem6  23285  lgslem4  23295  lgsneg  23315  lgsmod  23317  lgsdilem  23318  lgsdir  23326  lgsdi  23328  lgsne0  23329  lgsquad3  23357  dchrvmasum2if  23403  midexlem  23770  colperpex  23805  lmieu  23820  nmcfnlbi  26497  elpreq  26941  disjdifprg  26959  xrge0npcan  27196  archiabl  27254  orngsqr  27307  esumcst  27561  hasheuni  27581  esumcvg  27582  ddemeas  27698  eulerpartlemgc  27791  eulerpartlemb  27797  plymulx  27995  signswmnd  28004  erdsze2lem1  28137  prod1  28503  prodss  28506  trpredlem1  28737  wl-cbvalnaed  29412  wl-nfeqfb  29417  itg2addnclem  29494  itg2addnclem2  29495  iblmulc2nc  29508  ftc1anclem5  29522  ftc1anc  29526  dvasin  29531  areacirclem5  29539  exmid2  29953  ttac  30435  pw2f1ocnv  30436  aomclem5  30461  isnumbasgrplem3  30511  iocmbl  30638  fnchoice  30801  ifeq123d  30833  fzisoeu  30896  fperiodmul  30900  upbdrech2  30904  ioondisj2  30908  iccdifprioo  30939  fmul01lt1lem1  30953  fmul01lt1lem2  30954  limciccioolb  30982  lptioo2  30992  lptioo1  30993  limcicciooub  30998  lptre2pt  31001  limcresiooub  31003  limcresioolb  31004  limcleqr  31005  coskpi2  31021  cosknegpi  31024  icccncfext  31045  cncfiooicclem1  31051  cncfiooicc  31052  cncfiooiccre  31053  dvbdfbdioolem2  31078  ioodvbdlimc1lem1  31080  ioodvbdlimc1lem2  31081  ioodvbdlimc1  31082  ioodvbdlimc2lem  31083  ioodvbdlimc2  31084  volioc  31109  itgioocnicc  31114  iblcncfioo  31115  stoweidlem14  31133  stoweidlem26  31145  stoweidlem28  31147  stoweidlem55  31174  stoweid  31182  stirlinglem5  31197  stirlinglem12  31204  dirkerper  31215  dirkertrigeqlem3  31219  dirkertrigeq  31220  dirkercncflem1  31222  dirkercncflem2  31223  dirkercncf  31226  fourierdlem9  31235  fourierdlem10  31236  fourierdlem12  31238  fourierdlem17  31243  fourierdlem24  31250  fourierdlem30  31256  fourierdlem31  31257  fourierdlem32  31258  fourierdlem33  31259  fourierdlem34  31260  fourierdlem35  31261  fourierdlem37  31263  fourierdlem40  31266  fourierdlem41  31267  fourierdlem42  31268  fourierdlem43  31269  fourierdlem44  31270  fourierdlem45  31271  fourierdlem46  31272  fourierdlem48  31274  fourierdlem49  31275  fourierdlem51  31277  fourierdlem54  31280  fourierdlem62  31288  fourierdlem64  31290  fourierdlem65  31291  fourierdlem70  31296  fourierdlem71  31297  fourierdlem73  31299  fourierdlem74  31300  fourierdlem75  31301  fourierdlem76  31302  fourierdlem78  31304  fourierdlem79  31305  fourierdlem80  31306  fourierdlem81  31307  fourierdlem82  31308  fourierdlem89  31315  fourierdlem91  31317  fourierdlem92  31318  fourierdlem93  31319  fourierdlem97  31323  fourierdlem101  31327  fourierdlem102  31328  fourierdlem103  31329  fourierdlem104  31330  fourierdlem107  31333  fourierdlem109  31335  fourierdlem114  31340  sqwvfoura  31348  sqwvfourb  31349  fourierswlem  31350  fouriersw  31351  sharhght  31368  3dim1  34138  3dim2  34139  3dim3  34140  3atlem3  34156  3atlem7  34160  lvolnle3at  34253  2lplnja  34290  paddasslem18  34508  lhpexle3lem  34682  4atex  34747  cdlemd5  34873  cdleme16  34956  cdleme20  34995  cdleme21j  35007  cdleme21  35008  cdleme32snaw  35106  cdleme32fvcl  35111  cdleme32le  35118  cdlemeg46gf  35204  cdleme48gfv  35208  cdleme50trn12  35223  cdlemg6  35294  cdlemg7N  35297  cdlemg38  35386  cdlemg46  35406  dibvalrel  35835  dihlss  35922  dihglblem5aN  35964  dihmeetbN  35975  dihmeetALTN  35999  dihatlat  36006  dihatexv  36010  dvh3dim2  36120  dvh3dim3N  36121  lclkrlem2h  36186  mapdh8d  36455  mapdh8g  36458  hdmap11lem2  36517
  Copyright terms: Public domain W3C validator