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

Theorem biimparc 293
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 158 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 122 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biantr  898  elrab3t  2770  difprsnss  3573  elpw2g  3990  elon2  4201  ideqg  4583  elrnmpt1s  4681  elrnmptg  4683  fun11iun  5268  eqfnfv2  5392  fmpt  5443  elunirn  5537  spc2ed  5990  tposfo2  6024  tposf12  6026  dom2lem  6479  enfii  6580  ac6sfi  6604  ltexprlemm  7149  elreal2  7358  fihasheqf1oi  10184
  Copyright terms: Public domain W3C validator