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

Theorem pm5.32ri 631
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 630 . 2  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
3 ancom 448 . 2  |-  ( ( ps  /\  ph )  <->  (
ph  /\  ps )
)
4 ancom 448 . 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  688  pm5.61  705  oranabs  845  pm5.36  867  2eu5  2362  ceqsralt  2986  ceqsrexbv  3083  reuind  3151  rabsn  3930  reusv2lem4  4484  reusv2lem5  4485  reusv7OLD  4492  dfoprab2  6122  fsplit  6666  xpsnen  7383  elfpw  7601  rankuni  8058  isprm2  13754  pjfval2  17976  neipeltop  18575  cmpfi  18853  isxms2  19865  ishl2  20724  pjimai  25403  isbndx  28525  pm13.193  29510  bj-snglc  32045  cdlemefrs29pre00  33612  cdlemefrs29cpre1  33615  dihglb2  34560
  Copyright terms: Public domain W3C validator