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

Theorem pm5.32d 446
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 biimp 117 . . . 4 ((𝜒𝜃) → (𝜒𝜃))
31, 2syl6 33 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
43imdistand 444 . 2 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
5 biimpr 129 . . . 4 ((𝜒𝜃) → (𝜃𝜒))
61, 5syl6 33 . . 3 (𝜑 → (𝜓 → (𝜃𝜒)))
76imdistand 444 . 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  447  pm5.32da  448  pm5.32  449  anbi2d  460  cbvex2  1909  cores  5104  isoini  5783  mpoeq123  5895  genpassl  7459  genpassu  7460  fzind  9300  btwnz  9304  elfzm11  10020  isprm2  12043  isprm3  12044  modprminv  12175  modprminveq  12176
  Copyright terms: Public domain W3C validator