MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.32rd Structured version   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  6811  oeeui  6845  omxpenlem  7209  wemapwe  7654  fin23lem26  8205  1idpr  8906  smueqlem  13002  tchcph  19194  isusgra0  21376  is2wlk  21565  eupath2lem3  21701  outsideofeu  26065  ftc1anclem6  26285  mrefg2  26761  rmydioph  27085  islssfg2  27146  elfz2z  28105  2pthwlkonot  28352  cvrval5  30212  cdleme0ex2N  31021  dihglb2  32140
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