MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.32ri Unicode version

Theorem pm5.32ri 621
Description: Distribution of implication over biconditional (inference rule). (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 620 . 2  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
3 ancom 439 . 2  |-  ( ( ps  /\  ph )  <->  (
ph  /\  ps )
)
4 ancom 439 . 2  |-  ( ( ch  /\  ph )  <->  (
ph  /\  ch )
)
52, 3, 43bitr4i 270 1  |-  ( ( ps  /\  ph )  <->  ( ch  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  anbi1i  678  pm5.61  695  oranabs  831  pm5.36  851  2eu5  2228  ceqsralt  2812  ceqsrexbv  2903  reuind  2969  rabsn  3698  reusv2lem4  4537  reusv2lem5  4538  reusv7OLD  4545  dfoprab2  5856  fsplit  6184  xpsnen  6941  elfpw  7152  rankuni  7530  isprm2  12760  pjfval2  16603  cmpfi  17129  isxms2  17988  ishl2  18781  pjimai  22748  isbndx  25905  pm13.193  27010  cdlemefrs29pre00  29851  cdlemefrs29cpre1  29854  dihglb2  30799
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator