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

Theorem pm5.32da 433
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 112 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32pm5.32d 431 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  rexbida  2338  reubida  2508  rmobida  2513  mpteq12f  3864  reuhypd  4230  funbrfv2b  5245  dffn5im  5246  eqfnfv2  5293  fndmin  5301  fniniseg  5314  rexsupp  5318  fmptco  5357  dff13  5434  riotabidva  5511  mpt2eq123dva  5593  mpt2eq3dva  5596  mpt2xopovel  5886  qliftfun  6218  erovlem  6228  xpcomco  6330  ltexpi  6492  dfplpq2  6509  axprecex  7011  zrevaddcl  8351  qrevaddcl  8675  icoshft  8958  fznn  9052  shftdm  9650  2shfti  9659
  Copyright terms: Public domain W3C validator