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  2366  ceqsralt  3117  ceqsrexbv  3218  reuind  3287  rabsn  4079  reusv2lem4  4638  reusv2lem5  4639  reusv7OLD  4646  dfoprab2  6325  fsplit  6887  xpsnen  7600  elfpw  7821  rankuni  8281  isprm2  14099  ismnd  15794  pjfval2  18610  neipeltop  19500  cmpfi  19778  isxms2  20821  ishl2  21680  usgraop  24219  pjimai  26964  isbndx  30250  pm13.193  31269  bj-snglc  34260  cdlemefrs29pre00  35844  cdlemefrs29cpre1  35847  dihglb2  36792
  Copyright terms: Public domain W3C validator