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

Theorem pm5.32d 438
Description: Distribution of implication over biconditional (deduction rule). (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 116 . . . 4  |-  ( ( ch  <->  th )  ->  ( ch  ->  th ) )
31, 2syl6 33 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
43imdistand 436 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( ps 
/\  th ) ) )
5 bi2 128 . . . 4  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
61, 5syl6 33 . . 3  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
76imdistand 436 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ( ps  /\ 
ch ) ) )
84, 7impbid 127 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:  pm5.32rd  439  pm5.32da  440  pm5.32  441  anbi2d  452  cbvex2  1839  cores  4848  isoini  5482  mpt2eq123  5589  genpassl  6765  genpassu  6766  fzind  8532  btwnz  8536  elfzm11  9173  isprm2  10632  isprm3  10633
  Copyright terms: Public domain W3C validator