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  53  imim3i  60  loowoz  101  cbv1  1674  ralimdaa  2433  reuss2  3260  finds2  4370  ssrel  4474  ssrel2  4476  ssrelrel  4486  funfvima2  5444  tfrlem1  5978  tfrlemi1  6002  tfr1onlemaccex  6018  tfrcllemaccex  6031  tfri3  6037  nneneq  6414  ac6sfi  6455  pitonn  7148  nnaddcl  8196  nnmulcl  8197  zaddcllempos  8539  zaddcllemneg  8541  peano5uzti  8606  uzind2  8610  fzind  8613  zindd  8616  uzaddcl  8825  exfzdc  9396  frec2uzltd  9555  frecuzrdgg  9568  iseqvalt  9602  iseqoveq  9610  iseqss  9611  iseqsst  9612  iseqfveq2  9614  iseqshft2  9618  monoord  9621  iseqsplit  9624  iseqcaopr3  9626  iseqid3s  9632  iseqid2  9634  iseqhomo  9635  iseqz  9636  expivallem  9644  expcllem  9654  expap0  9673  mulexp  9682  expadd  9685  expmul  9688  leexp2r  9697  leexp1a  9698  bernneq  9760  facdiv  9832  facwordi  9834  faclbnd  9835  faclbnd6  9838  omgadd  9896  cjexp  9999  resqrexlemover  10115  resqrexlemdecn  10117  resqrexlemlo  10118  resqrexlemcalc3  10121  absexp  10184  dvdsfac  10486  gcdmultiple  10634  rplpwr  10641  nn0seqcvgd  10648  ialginv  10654  ialgcvga  10658  ialgfx  10659  prmdvdsexp  10752  prmfac1  10756
  Copyright terms: Public domain W3C validator