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

Theorem pm5.32da 440
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)
Hypothesis
Ref Expression
pm5.32da.1  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
Assertion
Ref Expression
pm5.32da  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )

Proof of Theorem pm5.32da
StepHypRef Expression
1 pm5.32da.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ch  <->  th )
)
21ex 113 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 438 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
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:  rexbida  2364  reubida  2536  rmobida  2541  mpteq12f  3866  reuhypd  4229  funbrfv2b  5250  dffn5im  5251  eqfnfv2  5298  fndmin  5306  fniniseg  5319  rexsupp  5323  fmptco  5362  dff13  5439  riotabidva  5515  mpt2eq123dva  5597  mpt2eq3dva  5600  mpt2xopovel  5890  qliftfun  6254  erovlem  6264  xpcomco  6370  ltexpi  6589  dfplpq2  6606  axprecex  7108  zrevaddcl  8482  qrevaddcl  8810  icoshft  9088  fznn  9182  shftdm  9848  2shfti  9857  sumeq2d  10334  sumeq2  10335  gcdaddm  10519
  Copyright terms: Public domain W3C validator