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

Theorem pm5.32da 425
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 9-Dec-2006.)
Hypothesis
Ref Expression
pm5.32da.1 ((φ ψ) → (χθ))
Assertion
Ref Expression
pm5.32da (φ → ((ψ χ) ↔ (ψ θ)))

Proof of Theorem pm5.32da
StepHypRef Expression
1 pm5.32da.1 . . 3 ((φ ψ) → (χθ))
21ex 108 . 2 (φ → (ψ → (χθ)))
32pm5.32d 423 1 (φ → ((ψ χ) ↔ (ψ θ)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  rexbida  2315  reubida  2485  rmobida  2490  mpteq12f  3828  reuhypd  4169  funbrfv2b  5161  dffn5im  5162  eqfnfv2  5209  fndmin  5217  fniniseg  5230  rexsupp  5234  fmptco  5273  dff13  5350  riotabidva  5427  mpt2eq123dva  5508  mpt2eq3dva  5511  mpt2xopovel  5797  qliftfun  6124  erovlem  6134  xpcomco  6236  ltexpi  6321  dfplpq2  6338  axprecex  6764  zrevaddcl  8071  qrevaddcl  8353  icoshft  8628  fznn  8721
  Copyright terms: Public domain W3C validator