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

Theorem pm5.32rd 645
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 644 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
3 ancom 452 . 2  |-  ( ( ch  /\  ps )  <->  ( ps  /\  ch )
)
4 ancom 452 . 2  |-  ( ( th  /\  ps )  <->  ( ps  /\  th )
)
52, 3, 43bitr4g 292 1  |-  ( ph  ->  ( ( ch  /\  ps )  <->  ( th  /\  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  anbi1d  710  pm5.71  945  omord  7279  oeeui  7313  omxpenlem  7681  wemapwe  8209  fin23lem26  8761  1idpr  9460  repsdf2  12881  smueqlem  14461  tchcph  22207  isusgra0  25070  is2wlk  25291  wwlkn0s  25429  wwlkextwrd  25452  clwwlkn2  25499  2pthwlkonot  25609  rusgranumwlkl1  25671  rusgra0edg  25679  eupath2lem3  25703  ordtconlem1  28736  outsideofeu  30901  ftc1anclem6  31984  cvrval5  32947  cdleme0ex2N  33757  dihglb2  34877  mrefg2  35516  rmydioph  35837  islssfg2  35897  elfz2z  38794  isusgr0  38924
  Copyright terms: Public domain W3C validator