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

Theorem pm5.32d 670
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 667 . 2 ((𝜓 → (𝜒𝜃)) ↔ ((𝜓𝜒) ↔ (𝜓𝜃)))
31, 2sylib 208 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  pm5.32rd  671  pm5.32da  672  anbi2d  739  raltpd  4285  cores  5597  isoini  6542  mpt2eq123  6667  ordpwsuc  6962  rdglim2  7473  fzind  11419  btwnz  11423  elfzm11  12352  isprm2  15319  isprm3  15320  modprminv  15428  modprminveq  15429  isrim  18654  elimifd  29206  funcnvmptOLD  29307  xrecex  29410  ordtconnlem1  29749  indpi1  29862  dfres3  31354  dfrdg4  31697  ee7.2aOLD  32099  wl-ax11-lem8  32998  expdioph  37067  pm14.122b  38103  rexbidar  38129  mapsnend  38862  isrngim  41189
  Copyright terms: Public domain W3C validator