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

Theorem pm5.32d 674
 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 671 . 2 ((𝜓 → (𝜒𝜃)) ↔ ((𝜓𝜒) ↔ (𝜓𝜃)))
31, 2sylib 208 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  pm5.32rd  675  pm5.32da  676  anbi2d  742  raltpd  4458  dfres3  5556  cores  5799  isoini  6751  mpt2eq123  6879  ordpwsuc  7180  rdglim2  7697  fzind  11667  btwnz  11671  elfzm11  12604  isprm2  15597  isprm3  15598  modprminv  15706  modprminveq  15707  isrim  18935  elimifd  29669  funcnvmptOLD  29776  xrecex  29937  ordtconnlem1  30279  indpi1  30391  dfrdg4  32364  ee7.2aOLD  32766  wl-ax11-lem8  33682  expdioph  38092  pm14.122b  39126  rexbidar  39152  mapsnend  39890  isrngim  42414
 Copyright terms: Public domain W3C validator