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

Theorem pm5.32ri 622
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 621 . 2  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
3 ancom 439 . 2  |-  ( ( ps  /\  ph )  <->  (
ph  /\  ps )
)
4 ancom 439 . 2  |-  ( ( ch  /\  ph )  <->  (
ph  /\  ch )
)
52, 3, 43bitr4i 270 1  |-  ( ( ps  /\  ph )  <->  ( ch  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  anbi1i  679  pm5.61  696  oranabs  832  pm5.36  854  2eu5  2200  ceqsralt  2779  ceqsrexbv  2870  reuind  2934  rabsn  3657  reusv2lem4  4496  reusv2lem5  4497  reusv7OLD  4504  dfoprab2  5815  fsplit  6143  xpsnen  6900  elfpw  7111  rankuni  7489  isprm2  12714  pjfval2  16557  cmpfi  17083  isxms2  17942  ishl2  18735  pjimai  22702  isbndx  25859  pm13.193  26965  cdlemefrs29pre00  29735  cdlemefrs29cpre1  29738  dihglb2  30683
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator