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  927  omord  7012  oeeui  7046  omxpenlem  7417  wemapwe  7933  wemapweOLD  7934  fin23lem26  8499  1idpr  9203  repsdf2  12421  smueqlem  13691  tchcph  20757  isusgra0  23280  is2wlk  23469  eupath2lem3  23605  ordtconlem1  26359  outsideofeu  28167  ftc1anclem6  28477  mrefg2  29048  rmydioph  29368  islssfg2  29429  elfz2z  30203  wwlkn0s  30344  wwlkextwrd  30365  2pthwlkonot  30409  clwwlkn2  30443  rusgranumwlkl1  30564  rusgra0edg  30578  cvrval5  33064  cdleme0ex2N  33873  dihglb2  34992
  Copyright terms: Public domain W3C validator