MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.32rd 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
Assertion
Ref Expression
pm5.32rd

Proof of Theorem pm5.32rd
StepHypRef Expression
1 pm5.32d.1 . . 3
21pm5.32d 639 . 2
3 ancom 450 . 2
4 ancom 450 . 2
52, 3, 43bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  anbi1d  704  pm5.71  936  omord  7236  oeeui  7270  omxpenlem  7638  wemapwe  8160  wemapweOLD  8161  fin23lem26  8726  1idpr  9428  repsdf2  12750  smueqlem  14140  tchcph  21680  isusgra0  24347  is2wlk  24567  wwlkn0s  24705  wwlkextwrd  24728  clwwlkn2  24775  2pthwlkonot  24885  rusgranumwlkl1  24947  rusgra0edg  24955  eupath2lem3  24979  ordtconlem1  27906  outsideofeu  29781  ftc1anclem6  30095  mrefg2  30639  rmydioph  30956  islssfg2  31017  elfz2z  32331  cvrval5  35139  cdleme0ex2N  35949  dihglb2  37069
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
  Copyright terms: Public domain W3C validator