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

Theorem pm5.32d 639
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 29-Oct-1996.)
Hypothesis
Ref Expression
pm5.32d.1
Assertion
Ref Expression
pm5.32d

Proof of Theorem pm5.32d
StepHypRef Expression
1 pm5.32d.1 . 2
2 pm5.32 636 . 2
31, 2sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  pm5.32rd  640  pm5.32da  641  anbi2d  703  cbvex2OLD  2029  raltpd  4153  cores  5515  isoini  6234  mpt2eq123  6356  ordpwsuc  6650  rdglim2  7117  fzind  10987  btwnz  10991  elfzm11  11778  isprm2  14225  isprm3  14226  modprminv  14326  modprminveq  14327  isrim  17382  elimifd  27421  funcnvmptOLD  27509  xrecex  27616  ordtconlem1  27906  indpi1  28035  dfres3  29188  dfrdg4  29600  ee7.2aOLD  29926  wl-ax11-lem8  30032  expdioph  30965  pm14.122b  31330  rexbidar  31355  isrngim  32710
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