ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimparc Unicode version

Theorem biimparc 297
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimparc  |-  ( ( ch  /\  ph )  ->  ps )

Proof of Theorem biimparc
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprcd 159 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 123 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biantr  937  elrab3t  2867  difprsnss  3694  elpw2g  4117  elon2  4336  ideqg  4737  elrnmpt1s  4836  elrnmptg  4838  fun11iun  5435  eqfnfv2  5566  fmpt  5617  elunirn  5716  spc2ed  6180  tposfo2  6214  tposf12  6216  dom2lem  6717  enfii  6819  ac6sfi  6843  ltexprlemm  7520  elreal2  7750  fihasheqf1oi  10662  fprod2dlemstep  11519  bastop2  12495
  Copyright terms: Public domain W3C validator