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

Theorem pm2.61dan 767
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 424 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61dan.2 . . 3  |-  ( (
ph  /\  -.  ps )  ->  ch )
43ex 424 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
52, 4pm2.61d 152 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359
This theorem is referenced by:  pm2.61ddan  768  pm2.61dda  769  nfsb4t  2127  ifeq1da  3764  ifeq2da  3765  ifclda  3766  ifbothda  3769  posn  4946  frsn  4948  somin1  5270  somincom  5271  xpcan  5305  fvmpti  5805  fvmptss  5813  funressn  5919  riotassuni  6588  oeoa  6840  oeoe  6842  omabs  6890  eceqoveq  7009  domdifsn  7191  pw2f1olem  7212  mapdom1  7272  marypha1lem  7438  infdifsn  7611  carden2b  7854  fidomtri  7880  dfac12lem2  8024  cdadom1  8066  infunsdom1  8093  infunsdom  8094  itunisuc  8299  gchdomtri  8504  xrmax2  10764  xrmin1  10765  ifle  10783  xmulneg1  10848  xrsupsslem  10885  xrinfmsslem  10886  fzneuz  11128  seqf1olem1  11362  bccmpl  11600  bcval5  11609  bcpasc  11612  bccl  11613  hasheni  11632  hashfn  11649  hashdom  11653  hashdomi  11654  hashge1  11663  hashbc  11702  sumz  12516  sumss  12518  sumsplit  12552  bitsmod  12948  sadadd2lem2  12962  sadcaddlem  12969  gcddvds  13015  gcdcl  13017  gcdneg  13026  pcgcd  13251  pcmpt  13261  pcmpt2  13262  pcprod  13264  fldivp1  13266  prmreclem4  13287  vdwlem6  13354  ramub1lem1  13394  cidpropd  13936  rescabs  14033  acsexdimd  14609  gsumval2  14783  gsumval3  15514  ablfac1c  15629  ablfac1eu  15631  mgpress  15659  psrbas  16443  resspsrbas  16478  mplmonmul  16527  mplcoe1  16528  mplcoe2  16530  opsrle  16536  opsrbaslem  16538  psrbaspropd  16628  mplbaspropd  16630  opnnei  17184  restbas  17222  hauspwdom  17564  ptcmplem5  18087  xrsmopn  18843  xrhmeo  18971  lebnum  18989  pcohtpylem  19044  pcoass  19049  pcorevlem  19051  icombl  19458  ioombl  19459  mbfconstlem  19521  mbfima  19524  i1fd  19573  mbfi1fseqlem5  19611  itg2const2  19633  itg2seq  19634  itg2uba  19635  itg2splitlem  19640  itg2split  19641  itg2monolem1  19642  itg2gt0  19652  itg2cnlem1  19653  itg2cnlem2  19654  iblss  19696  iblss2  19697  itgss  19703  bddmulibl  19730  coemullem  20168  aaliou2b  20258  isppw2  20898  mule1  20931  ppip1le  20944  dchrelbas3  21022  dchrpt  21051  bposlem3  21070  bposlem5  21072  bposlem6  21073  lgslem4  21083  lgsneg  21103  lgsmod  21105  lgsdilem  21106  lgsdir  21114  lgsdi  21116  lgsne0  21117  lgsquad3  21145  dchrvmasum2if  21191  nmcfnlbi  23555  elpreq  23999  disjdifprg  24017  xrge0npcan  24216  gsumpropd2lem  24220  ofldsqr  24240  esumcst  24455  hasheuni  24475  esumcvg  24476  erdsze2lem1  24889  prod1  25270  prodss  25273  trpredlem1  25505  itg2addnclem  26256  itg2addnclem2  26257  iblmulc2nc  26270  ftc1anclem5  26284  ftc1anc  26288  areacirclem5  26296  ttac  27107  pw2f1ocnv  27108  aomclem5  27133  frlmsslsp  27225  isnumbasgrplem3  27247  f1otrspeq  27367  pmtrfinv  27379  psgnunilem1  27393  fnchoice  27676  fmul01lt1lem1  27690  fmul01lt1lem2  27691  stoweidlem14  27739  stoweidlem26  27751  stoweidlem28  27753  stoweidlem55  27780  stoweid  27788  stirlinglem5  27803  stirlinglem12  27810  sharhght  27831  ifeqda  28052  2if2  28053  3dim1  30264  3dim2  30265  3dim3  30266  3atlem3  30282  3atlem7  30286  lvolnle3at  30379  2lplnja  30416  paddasslem18  30634  lhpexle3lem  30808  4atex  30873  cdlemd5  30999  cdleme16  31082  cdleme20  31121  cdleme21j  31133  cdleme21  31134  cdleme32snaw  31232  cdleme32fvcl  31237  cdleme32le  31244  cdlemeg46gf  31330  cdleme48gfv  31334  cdleme50trn12  31349  cdlemg6  31420  cdlemg7N  31423  cdlemg38  31512  cdlemg46  31532  dibvalrel  31961  dihlss  32048  dihglblem5aN  32090  dihmeetbN  32101  dihmeetALTN  32125  dihatlat  32132  dihatexv  32136  dvh3dim2  32246  dvh3dim3N  32247  lclkrlem2h  32312  mapdh8d  32581  mapdh8g  32584  hdmap11lem2  32643
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 178  df-an 361
  Copyright terms: Public domain W3C validator