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

Theorem pm5.32rd 622
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 621 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
3 ancom 438 . 2  |-  ( ( ch  /\  ps )  <->  ( ps  /\  ch )
)
4 ancom 438 . 2  |-  ( ( th  /\  ps )  <->  ( ps  /\  th )
)
52, 3, 43bitr4g 280 1  |-  ( ph  ->  ( ( ch  /\  ps )  <->  ( th  /\  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  anbi1d  686  pm5.71  903  omord  6770  oeeui  6804  omxpenlem  7168  wemapwe  7610  fin23lem26  8161  1idpr  8862  smueqlem  12957  tchcph  19147  isusgra0  21329  is2wlk  21518  eupath2lem3  21654  outsideofeu  25969  mrefg2  26651  rmydioph  26975  islssfg2  27037  2pthwlkonot  28082  cvrval5  29897  cdleme0ex2N  30706  dihglb2  31825
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