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 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 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  2368  reubida  2540  rmobida  2545  mpteq12f  3878  reuhypd  4249  funbrfv2b  5271  dffn5im  5272  eqfnfv2  5319  fndmin  5327  fniniseg  5340  rexsupp  5344  fmptco  5383  dff13  5460  riotabidva  5536  mpt2eq123dva  5618  mpt2eq3dva  5621  mpt2xopovel  5911  qliftfun  6276  erovlem  6286  xpcomco  6392  ltexpi  6659  dfplpq2  6676  axprecex  7178  zrevaddcl  8552  qrevaddcl  8880  icoshft  9158  fznn  9252  shftdm  9929  2shfti  9938  sumeq2d  10415  sumeq2  10416  gcdaddm  10600
  Copyright terms: Public domain W3C validator