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  854  pm5.36  877  2eu5  2392  ceqsralt  3142  ceqsrexbv  3243  reuind  3312  rabsn  4100  reusv2lem4  4657  reusv2lem5  4658  reusv7OLD  4665  dfoprab2  6338  fsplit  6900  xpsnen  7613  elfpw  7834  rankuni  8293  isprm2  14101  ismnd  15797  pjfval2  18609  neipeltop  19498  cmpfi  19776  isxms2  20819  ishl2  21678  usgraop  24173  pjimai  26918  isbndx  30205  pm13.193  31220  bj-snglc  34009  cdlemefrs29pre00  35592  cdlemefrs29cpre1  35595  dihglb2  36540
  Copyright terms: Public domain W3C validator