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  2197  ceqsralt  2749  ceqsrexbv  2839  reuind  2903  rabsn  3601  reusv2lem4  4429  reusv2lem5  4430  reusv7OLD  4437  dfoprab2  5747  fsplit  6075  xpsnen  6831  elfpw  7041  rankuni  7419  isprm2  12640  pjfval2  16441  cmpfi  16967  isxms2  17826  ishl2  18619  pjimai  22586  isbndx  25672  pm13.193  26778  cdlemefrs29pre00  29488  cdlemefrs29cpre1  29491  dihglb2  30436
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