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

Theorem a2d 26
Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)
Hypothesis
Ref Expression
a2d.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
a2d (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))

Proof of Theorem a2d
StepHypRef Expression
1 a2d.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 ax-2 6 . 2 ((𝜓 → (𝜒𝜃)) → ((𝜓𝜒) → (𝜓𝜃)))
31, 2syl 14 1 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  mpdd  40  imim2d  52  imim3i  59  loowoz  100  cbv1  1648  ralimdaa  2403  reuss2  3244  finds2  4351  ssrel  4455  ssrel2  4457  ssrelrel  4467  funfvima2  5418  tfrlem1  5953  tfrlemi1  5976  tfri3  5983  rdgon  6003  nneneq  6350  ac6sfi  6382  pitonn  6981  nnaddcl  8009  nnmulcl  8010  zaddcllempos  8338  zaddcllemneg  8340  peano5uzti  8404  uzind2  8408  fzind  8411  zindd  8414  uzaddcl  8624  frec2uzltd  9352  iseqss  9389  iseqfveq2  9391  iseqshft2  9395  monoord  9398  iseqsplit  9401  iseqcaopr3  9403  iseqid3s  9409  iseqhomo  9411  iseqz  9412  expivallem  9420  expcllem  9430  expap0  9449  mulexp  9458  expadd  9461  expmul  9464  leexp2r  9473  leexp1a  9474  bernneq  9536  facdiv  9605  facwordi  9607  faclbnd  9608  faclbnd6  9611  cjexp  9720  resqrexlemover  9836  resqrexlemdecn  9838  resqrexlemlo  9839  resqrexlemcalc3  9842  absexp  9905  dvdsfac  10171  nn0seqcvgd  10242  ialginv  10248  ialgcvga  10252  ialgfx  10253
  Copyright terms: Public domain W3C validator