Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm5.32d GIF version

Theorem pm5.32d 443
 Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.) (Revised by NM, 31-Jan-2015.)
Hypothesis
Ref Expression
pm5.32d.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
pm5.32d (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))

Proof of Theorem pm5.32d
StepHypRef Expression
1 pm5.32d.1 . . . 4 (𝜑 → (𝜓 → (𝜒𝜃)))
2 bi1 117 . . . 4 ((𝜒𝜃) → (𝜒𝜃))
31, 2syl6 33 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
43imdistand 441 . 2 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
5 bi2 129 . . . 4 ((𝜒𝜃) → (𝜃𝜒))
61, 5syl6 33 . . 3 (𝜑 → (𝜓 → (𝜃𝜒)))
76imdistand 441 . 2 (𝜑 → ((𝜓𝜃) → (𝜓𝜒)))
84, 7impbid 128 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  pm5.32rd  444  pm5.32da  445  pm5.32  446  anbi2d  457  cbvex2  1872  cores  5010  isoini  5685  mpoeq123  5796  genpassl  7296  genpassu  7297  fzind  9120  btwnz  9124  elfzm11  9822  isprm2  11705  isprm3  11706
 Copyright terms: Public domain W3C validator