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

Theorem pm5.32d 669
 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 666 . 2 ((𝜓 → (𝜒𝜃)) ↔ ((𝜓𝜒) ↔ (𝜓𝜃)))
31, 2sylib 207 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385 This theorem is referenced by:  pm5.32rd  670  pm5.32da  671  anbi2d  736  raltpd  4258  cores  5555  isoini  6488  mpt2eq123  6612  ordpwsuc  6907  rdglim2  7415  fzind  11351  btwnz  11355  elfzm11  12280  isprm2  15233  isprm3  15234  modprminv  15342  modprminveq  15343  isrim  18556  elimifd  28746  funcnvmptOLD  28850  xrecex  28959  ordtconlem1  29298  indpi1  29411  dfres3  30902  dfrdg4  31228  ee7.2aOLD  31630  wl-ax11-lem8  32548  expdioph  36608  pm14.122b  37646  rexbidar  37671  mapsnend  38386  isrngim  41694
 Copyright terms: Public domain W3C validator