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

Theorem pm5.32d 580
 Description: Distribution of implication over biconditional (deduction form). (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 577 . 2 ((𝜓 → (𝜒𝜃)) ↔ ((𝜓𝜒) ↔ (𝜓𝜃)))
31, 2sylib 221 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  pm5.32rd  581  pm5.32da  582  anbi2d  631  ralrexbid  3284  raltpd  4680  opeqsng  5361  dfres3  5827  cores  6073  isoini  7074  mpoeq123  7209  ordpwsuc  7514  rdglim2  8055  fzind  12072  btwnz  12076  elfzm11  12977  isprm2  16019  isprm3  16020  modprminv  16129  modprminveq  16130  isrim  19484  elimifd  30313  xrecex  30625  ordtconnlem1  31275  indpi1  31387  eqfunresadj  33112  dfrdg4  33520  ee7.2aOLD  33917  wl-ax11-lem8  34982  expdioph  39951  pm14.122b  41114  rexbidar  41137  isrngim  44515
 Copyright terms: Public domain W3C validator