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  936  elrab3t  2834  difprsnss  3653  elpw2g  4076  elon2  4293  ideqg  4685  elrnmpt1s  4784  elrnmptg  4786  fun11iun  5381  eqfnfv2  5512  fmpt  5563  elunirn  5660  spc2ed  6123  tposfo2  6157  tposf12  6159  dom2lem  6659  enfii  6761  ac6sfi  6785  ltexprlemm  7401  elreal2  7631  fihasheqf1oi  10527  bastop2  12242
  Copyright terms: Public domain W3C validator