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

Theorem pm5.32ri 455
Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 12-Mar-1995.)
Hypothesis
Ref Expression
pm5.32i.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
pm5.32ri  |-  ( ( ps  /\  ph )  <->  ( ch  /\  ph )
)

Proof of Theorem pm5.32ri
StepHypRef Expression
1 pm5.32i.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21pm5.32i 454 . 2  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
3 ancom 266 . 2  |-  ( ( ps  /\  ph )  <->  (
ph  /\  ps )
)
4 ancom 266 . 2  |-  ( ( ch  /\  ph )  <->  (
ph  /\  ch )
)
52, 3, 43bitr4i 212 1  |-  ( ( ps  /\  ph )  <->  ( ch  /\  ph )
)
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:  anbi1i  458  pm5.36  610  pm5.61  794  oranabs  815  ceqsralt  2765  ceqsrexbv  2869  reuind  2943  rabsn  3660  dfoprab2  5922  xpsnen  6821  nn1suc  8938  isprm2  12117  ismnd  12820  dfgrp2e  12903  isxms2  13955
  Copyright terms: Public domain W3C validator