Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm5.32da 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  2321  reubida  2491  rmobida  2496  mpteq12f  3837  reuhypd  4203  funbrfv2b  5218  dffn5im  5219  eqfnfv2  5266  fndmin  5274  fniniseg  5287  rexsupp  5291  fmptco  5330  dff13  5407  riotabidva  5484  mpt2eq123dva  5566  mpt2eq3dva  5569  mpt2xopovel  5856  qliftfun  6188  erovlem  6198  xpcomco  6300  ltexpi  6435  dfplpq2  6452  axprecex  6954  zrevaddcl  8295  qrevaddcl  8578  icoshft  8858  fznn  8951  shftdm  9423  2shfti  9432
 Copyright terms: Public domain W3C validator