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 form). (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  2375  reubida  2548  rmobida  2553  mpteq12f  3918  reuhypd  4293  funbrfv2b  5349  dffn5im  5350  eqfnfv2  5398  fndmin  5406  fniniseg  5419  rexsupp  5423  fmptco  5464  dff13  5547  riotabidva  5624  mpt2eq123dva  5710  mpt2eq3dva  5713  mpt2xopovel  6006  qliftfun  6374  erovlem  6384  xpcomco  6542  ltexpi  6896  dfplpq2  6913  axprecex  7415  zrevaddcl  8800  qrevaddcl  9129  icoshft  9407  fznn  9503  shftdm  10256  2shfti  10265  sumeq2  10748  fisum  10778  fsum2dlemstep  10828  gcdaddm  11253  elcncf2  11630
  Copyright terms: Public domain W3C validator