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

Theorem pm5.32ri 620
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 619 . 2  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
3 ancom 438 . 2  |-  ( ( ps  /\  ph )  <->  (
ph  /\  ps )
)
4 ancom 438 . 2  |-  ( ( ch  /\  ph )  <->  (
ph  /\  ch )
)
52, 3, 43bitr4i 269 1  |-  ( ( ps  /\  ph )  <->  ( ch  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  anbi1i  677  pm5.61  694  oranabs  830  pm5.36  850  2eu5  2364  ceqsralt  2971  ceqsrexbv  3062  reuind  3129  rabsn  3865  reusv2lem4  4719  reusv2lem5  4720  reusv7OLD  4727  dfoprab2  6113  fsplit  6443  xpsnen  7184  elfpw  7400  rankuni  7781  isprm2  13079  pjfval2  16928  neipeltop  17185  cmpfi  17463  isxms2  18470  ishl2  19316  pjimai  23671  isbndx  26482  pm13.193  27579  cdlemefrs29pre00  31129  cdlemefrs29cpre1  31132  dihglb2  32077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator