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

Theorem pm5.32d 450
Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.) (Revised by NM, 31-Jan-2015.)
Hypothesis
Ref Expression
pm5.32d.1  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
Assertion
Ref Expression
pm5.32d  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )

Proof of Theorem pm5.32d
StepHypRef Expression
1 pm5.32d.1 . . . 4  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
2 biimp 118 . . . 4  |-  ( ( ch  <->  th )  ->  ( ch  ->  th ) )
31, 2syl6 33 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
43imdistand 447 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( ps 
/\  th ) ) )
5 biimpr 130 . . . 4  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
61, 5syl6 33 . . 3  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
76imdistand 447 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ps  /\ 
ch ) ) )
84, 7impbid 129 1  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm5.32rd  451  pm5.32da  452  pm5.32  453  anbi2d  464  cbvex2  1922  cores  5134  isoini  5821  mpoeq123  5936  genpassl  7525  genpassu  7526  fzind  9370  btwnz  9374  elfzm11  10093  isprm2  12119  isprm3  12120  modprminv  12251  modprminveq  12252
  Copyright terms: Public domain W3C validator