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

Theorem pm5.32rd 640
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 25-Dec-2004.)
Hypothesis
Ref Expression
pm5.32d.1  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
Assertion
Ref Expression
pm5.32rd  |-  ( ph  ->  ( ( ch  /\  ps )  <->  ( th  /\  ps ) ) )

Proof of Theorem pm5.32rd
StepHypRef Expression
1 pm5.32d.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch 
<->  th ) ) )
21pm5.32d 639 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
3 ancom 450 . 2  |-  ( ( ch  /\  ps )  <->  ( ps  /\  ch )
)
4 ancom 450 . 2  |-  ( ( th  /\  ps )  <->  ( ps  /\  th )
)
52, 3, 43bitr4g 288 1  |-  ( ph  ->  ( ( ch  /\  ps )  <->  ( th  /\  ps ) ) )
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:  anbi1d  704  pm5.71  936  omord  7219  oeeui  7253  omxpenlem  7620  wemapwe  8142  wemapweOLD  8143  fin23lem26  8708  1idpr  9410  repsdf2  12729  smueqlem  14017  tchcph  21553  isusgra0  24219  is2wlk  24439  wwlkn0s  24577  wwlkextwrd  24600  clwwlkn2  24647  2pthwlkonot  24757  rusgranumwlkl1  24819  rusgra0edg  24827  eupath2lem3  24851  ordtconlem1  27779  outsideofeu  29756  ftc1anclem6  30070  mrefg2  30614  rmydioph  30931  islssfg2  30992  elfz2z  32169  cvrval5  34873  cdleme0ex2N  35683  dihglb2  36803
  Copyright terms: Public domain W3C validator