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

Theorem pm5.32ri 619
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 618 . 2  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
3 ancom 437 . 2  |-  ( ( ps  /\  ph )  <->  (
ph  /\  ps )
)
4 ancom 437 . 2  |-  ( ( ch  /\  ph )  <->  (
ph  /\  ch )
)
52, 3, 43bitr4i 268 1  |-  ( ( ps  /\  ph )  <->  ( ch  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  anbi1i  676  pm5.61  693  oranabs  829  pm5.36  849  2eu5  2227  ceqsralt  2811  ceqsrexbv  2902  reuind  2968  rabsn  3697  reusv2lem4  4538  reusv2lem5  4539  reusv7OLD  4546  dfoprab2  5895  fsplit  6223  xpsnen  6946  elfpw  7157  rankuni  7535  isprm2  12766  pjfval2  16609  cmpfi  17135  isxms2  17994  ishl2  18787  pjimai  22756  isbndx  25918  pm13.193  27023  cdlemefrs29pre00  29957  cdlemefrs29cpre1  29960  dihglb2  30905
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator