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

Theorem pm5.32ri 642
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 641 . 2  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
3 ancom 451 . 2  |-  ( ( ps  /\  ph )  <->  (
ph  /\  ps )
)
4 ancom 451 . 2  |-  ( ( ch  /\  ph )  <->  (
ph  /\  ch )
)
52, 3, 43bitr4i 280 1  |-  ( ( ps  /\  ph )  <->  ( ch  /\  ph )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  anbi1i  699  pm5.61  717  oranabs  864  pm5.36  887  2eu5  2355  ceqsralt  3105  ceqsrexbv  3206  reuind  3275  rabsn  4064  reusv2lem4  4625  reusv2lem5  4626  dfoprab2  6348  fsplit  6909  xpsnen  7659  elfpw  7879  rankuni  8336  isprm2  14620  ismnd  16527  pjfval2  19259  neipeltop  20132  cmpfi  20410  isxms2  21450  ishl2  22324  usgraop  25064  pjimai  27815  bj-snglc  31519  isbndx  32028  cdlemefrs29pre00  33881  cdlemefrs29cpre1  33884  dihglb2  34829  pm13.193  36620
  Copyright terms: Public domain W3C validator