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

Theorem pm5.32da 440
Description: Distribution of implication over biconditional (deduction form). (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 113 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32pm5.32d 438 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  rexbida  2375  reubida  2548  rmobida  2553  mpteq12f  3918  reuhypd  4293  funbrfv2b  5349  dffn5im  5350  eqfnfv2  5398  fndmin  5406  fniniseg  5419  rexsupp  5423  fmptco  5464  dff13  5547  riotabidva  5624  mpt2eq123dva  5710  mpt2eq3dva  5713  mpt2xopovel  6006  qliftfun  6372  erovlem  6382  xpcomco  6540  ltexpi  6894  dfplpq2  6911  axprecex  7413  zrevaddcl  8798  qrevaddcl  9127  icoshft  9405  fznn  9499  shftdm  10252  2shfti  10261  sumeq2  10744  fisum  10774  fsum2dlemstep  10824  gcdaddm  11249  elcncf2  11585
  Copyright terms: Public domain W3C validator