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  934  omord  7229  oeeui  7263  omxpenlem  7630  wemapwe  8151  wemapweOLD  8152  fin23lem26  8717  1idpr  9419  repsdf2  12730  smueqlem  14016  tchcph  21548  isusgra0  24161  is2wlk  24381  wwlkn0s  24519  wwlkextwrd  24542  clwwlkn2  24589  2pthwlkonot  24699  rusgranumwlkl1  24761  rusgra0edg  24769  eupath2lem3  24793  ordtconlem1  27722  outsideofeu  29699  ftc1anclem6  30013  mrefg2  30558  rmydioph  30875  islssfg2  30936  elfz2z  32112  cvrval5  34567  cdleme0ex2N  35376  dihglb2  36495
  Copyright terms: Public domain W3C validator