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

Theorem pm5.32ri 638
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 637 . 2  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
3 ancom 450 . 2  |-  ( ( ps  /\  ph )  <->  (
ph  /\  ps )
)
4 ancom 450 . 2  |-  ( ( ch  /\  ph )  <->  (
ph  /\  ch )
)
52, 3, 43bitr4i 277 1  |-  ( ( ps  /\  ph )  <->  ( ch  /\  ph )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  anbi1i  695  pm5.61  712  oranabs  852  pm5.36  874  2eu5  2379  ceqsralt  3102  ceqsrexbv  3201  reuind  3270  rabsn  4053  reusv2lem4  4607  reusv2lem5  4608  reusv7OLD  4615  dfoprab2  6245  fsplit  6790  xpsnen  7508  elfpw  7727  rankuni  8185  isprm2  13893  pjfval2  18269  neipeltop  18875  cmpfi  19153  isxms2  20165  ishl2  21024  pjimai  25759  isbndx  28852  pm13.193  29836  bj-snglc  32819  cdlemefrs29pre00  34402  cdlemefrs29cpre1  34405  dihglb2  35350
  Copyright terms: Public domain W3C validator