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

Theorem pm5.32da 449
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 447 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  2465  reubida  2651  rmobida  2656  mpteq12f  4069  reuhypd  4456  funbrfv2b  5541  dffn5im  5542  eqfnfv2  5594  fndmin  5603  fniniseg  5616  rexsupp  5620  fmptco  5662  dff13  5747  riotabidva  5825  mpoeq123dva  5914  mpoeq3dva  5917  mpoxopovel  6220  qliftfun  6595  erovlem  6605  xpcomco  6804  elfi2  6949  ctssdccl  7088  ltexpi  7299  dfplpq2  7316  axprecex  7842  zrevaddcl  9262  qrevaddcl  9603  icoshft  9947  fznn  10045  shftdm  10786  2shfti  10795  sumeq2  11322  fsum3  11350  fsum2dlemstep  11397  prodeq2  11520  fprodseq  11546  gcdaddm  11939  grpidpropdg  12628  ismgmid  12631  mhmpropd  12689  bastop2  12878  restopn2  12977  iscnp3  12997  lmbr2  13008  txlm  13073  ismet2  13148  xblpnfps  13192  xblpnf  13193  blininf  13218  blres  13228  elmopn2  13243  neibl  13285  metrest  13300  metcnp3  13305  metcnp  13306  metcnp2  13307  metcn  13308  txmetcn  13313  cnbl0  13328  cnblcld  13329  bl2ioo  13336  elcncf2  13355  cncfmet  13373  cnlimc  13435
  Copyright terms: Public domain W3C validator