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  947  elrab3t  2885  difprsnss  3718  elpw2g  4142  elon2  4361  ideqg  4762  elrnmpt1s  4861  elrnmptg  4863  fun11iun  5463  eqfnfv2  5594  fmpt  5646  elunirn  5745  spc2ed  6212  tposfo2  6246  tposf12  6248  dom2lem  6750  enfii  6852  ac6sfi  6876  ltexprlemm  7562  elreal2  7792  fihasheqf1oi  10722  fprod2dlemstep  11585  bastop2  12878
  Copyright terms: Public domain W3C validator