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

Theorem simplbi2 623
Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
Hypothesis
Ref Expression
simplbi2.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
simplbi2  |-  ( ps 
->  ( ch  ->  ph )
)

Proof of Theorem simplbi2
StepHypRef Expression
1 simplbi2.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpri 206 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 432 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  simplbi2com  625  sspss  3589  neldif  3615  reuss2  3775  pssdifn0  3876  ordunidif  4915  eceqoveq  7408  infxpenlem  8382  ackbij1lem18  8608  isf32lem2  8725  ingru  9182  indpi  9274  nqereu  9296  elfz0ubfz0  11782  elfzmlbp  11790  fzo1fzo0n0  11841  elfzo0z  11842  fzofzim  11846  elfzodifsumelfzo  11863  2swrd1eqwrdeq  12673  swrdswrd  12679  swrdccatin1  12702  swrd2lsw  12884  algcvga  14295  pcprendvds  14451  restntr  19853  filcon  20553  filssufilg  20581  ufileu  20589  ufilen  20600  alexsubALTlem3  20718  blcld  21177  causs  21906  itg2addlem  22334  rplogsum  23913  sizeusglecusglem1  24689  clwlkisclwwlklem1  24992  clwwlknwwlkncl  25005  numclwwlk2lem1  25307  ofpreima2  27738  esumpinfval  28305  eulerpartlemf  28576  sltres  29667  fin2so  30283  fdc  30481  ndmaovass  32533  elfz2z  32724  usgra2pth  32745  onfrALTlem2  33731  3ornot23VD  34066  ordelordALTVD  34087  onfrALTlem2VD  34109  bj-elid2  35020  lshpcmp  35129  lfl1  35211
  Copyright terms: Public domain W3C validator