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

Theorem pm2.61ian 788
Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
pm2.61ian.1  |-  ( (
ph  /\  ps )  ->  ch )
pm2.61ian.2  |-  ( ( -.  ph  /\  ps )  ->  ch )
Assertion
Ref Expression
pm2.61ian  |-  ( ps 
->  ch )

Proof of Theorem pm2.61ian
StepHypRef Expression
1 pm2.61ian.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 434 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61ian.2 . . 3  |-  ( ( -.  ph  /\  ps )  ->  ch )
43ex 434 . 2  |-  ( -. 
ph  ->  ( ps  ->  ch ) )
52, 4pm2.61i 164 1  |-  ( ps 
->  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:  4cases  947  consensus  957  cases2  970  ax12indalem  2268  sbcrext  3414  csbexg  4579  xpcan2  5443  tfindsg  6674  findsg  6706  ixpexg  7493  fipwss  7888  ranklim  8261  fin23lem14  8712  fzoval  11797  hashge2el2dif  12486  iswrdi  12517  ffz0iswrd  12533  swrd0  12620  swrdspsleq  12635  swrdccatin12  12678  swrdccat  12680  repswswrd  12718  cshword  12724  cshwcsh2id  12758  ressbas  14544  resslem  14547  ressinbas  14550  cntzval  16161  symg2bas  16225  sralem  17618  srasca  17622  sravsca  17623  sraip  17624  ocvval  18481  dsmmval  18548  dmatmul  18782  1mavmul  18833  mavmul0g  18838  1marepvmarrepid  18860  smadiadetglem2  18957  1elcpmat  18999  decpmatid  19054  tnglem  20905  tngds  20913  clwlkisclwwlklem2a4  24476  clwlkisclwwlklem2a  24477  clwwisshclwwn  24500  unopbd  26626  nmopcoi  26706  resvsca  27499  resvlem  27500  afvres  31740  afvco2  31744  2ffzoeq  31824  ply1mulgsumlem2  32077  lcoel0  32119  lindslinindsimp1  32148
  Copyright terms: Public domain W3C validator