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

Theorem pm5.32rd 638
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 637 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  <->  ( ps  /\  th ) ) )
3 ancom 448 . 2  |-  ( ( ch  /\  ps )  <->  ( ps  /\  ch )
)
4 ancom 448 . 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 367
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 369
This theorem is referenced by:  anbi1d  702  pm5.71  934  omord  7135  oeeui  7169  omxpenlem  7537  wemapwe  8052  wemapweOLD  8053  fin23lem26  8618  1idpr  9318  repsdf2  12661  smueqlem  14142  tchcph  21765  isusgra0  24468  is2wlk  24688  wwlkn0s  24826  wwlkextwrd  24849  clwwlkn2  24896  2pthwlkonot  25006  rusgranumwlkl1  25068  rusgra0edg  25076  eupath2lem3  25100  ordtconlem1  28060  outsideofeu  29934  ftc1anclem6  30261  mrefg2  30805  rmydioph  31122  islssfg2  31183  elfz2z  32652  cvrval5  35552  cdleme0ex2N  36362  dihglb2  37482
  Copyright terms: Public domain W3C validator