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

Theorem pm5.32da 448
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 114 . 2  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
32pm5.32d 446 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
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:  rexbida  2433  reubida  2615  rmobida  2620  mpteq12f  4015  reuhypd  4399  funbrfv2b  5473  dffn5im  5474  eqfnfv2  5526  fndmin  5534  fniniseg  5547  rexsupp  5551  fmptco  5593  dff13  5676  riotabidva  5753  mpoeq123dva  5839  mpoeq3dva  5842  mpoxopovel  6145  qliftfun  6518  erovlem  6528  xpcomco  6727  elfi2  6867  ctssdccl  7003  ltexpi  7168  dfplpq2  7185  axprecex  7711  zrevaddcl  9127  qrevaddcl  9462  icoshft  9802  fznn  9899  shftdm  10625  2shfti  10634  sumeq2  11159  fsum3  11187  fsum2dlemstep  11234  prodeq2  11357  gcdaddm  11706  bastop2  12290  restopn2  12389  iscnp3  12409  lmbr2  12420  txlm  12485  ismet2  12560  xblpnfps  12604  xblpnf  12605  blininf  12630  blres  12640  elmopn2  12655  neibl  12697  metrest  12712  metcnp3  12717  metcnp  12718  metcnp2  12719  metcn  12720  txmetcn  12725  cnbl0  12740  cnblcld  12741  bl2ioo  12748  elcncf2  12767  cncfmet  12785  cnlimc  12847
  Copyright terms: Public domain W3C validator