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

Theorem pm5.32d 445
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 bi1 117 . . . 4  |-  ( ( ch  <->  th )  ->  ( ch  ->  th ) )
31, 2syl6 33 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
43imdistand 443 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( ps 
/\  th ) ) )
5 bi2 129 . . . 4  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
61, 5syl6 33 . . 3  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
76imdistand 443 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ps  /\ 
ch ) ) )
84, 7impbid 128 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:  pm5.32rd  446  pm5.32da  447  pm5.32  448  anbi2d  459  cbvex2  1874  cores  5012  isoini  5687  mpoeq123  5798  genpassl  7300  genpassu  7301  fzind  9134  btwnz  9138  elfzm11  9839  isprm2  11725  isprm3  11726
  Copyright terms: Public domain W3C validator