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

Theorem pm5.32da 447
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 114 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32pm5.32d 445 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  rexbida  2409  reubida  2589  rmobida  2594  mpteq12f  3978  reuhypd  4362  funbrfv2b  5434  dffn5im  5435  eqfnfv2  5487  fndmin  5495  fniniseg  5508  rexsupp  5512  fmptco  5554  dff13  5637  riotabidva  5714  mpoeq123dva  5800  mpoeq3dva  5803  mpoxopovel  6106  qliftfun  6479  erovlem  6489  xpcomco  6688  elfi2  6828  ctssdccl  6964  ltexpi  7113  dfplpq2  7130  axprecex  7656  zrevaddcl  9072  qrevaddcl  9404  icoshft  9741  fznn  9837  shftdm  10562  2shfti  10571  sumeq2  11096  fsum3  11124  fsum2dlemstep  11171  gcdaddm  11599  bastop2  12180  restopn2  12279  iscnp3  12299  lmbr2  12310  txlm  12375  ismet2  12450  xblpnfps  12494  xblpnf  12495  blininf  12520  blres  12530  elmopn2  12545  neibl  12587  metrest  12602  metcnp3  12607  metcnp  12608  metcnp2  12609  metcn  12610  txmetcn  12615  cnbl0  12630  cnblcld  12631  bl2ioo  12638  elcncf2  12657  cncfmet  12675  cnlimc  12737
  Copyright terms: Public domain W3C validator