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

Theorem a2d 26
Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)
Hypothesis
Ref Expression
a2d.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
a2d  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )

Proof of Theorem a2d
StepHypRef Expression
1 a2d.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
2 ax-2 6 . 2  |-  ( ( ps  ->  ( ch  ->  th ) )  -> 
( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
31, 2syl 14 1  |-  ( ph  ->  ( ( ps  ->  ch )  ->  ( ps  ->  th ) ) )
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  3245  finds2  4352  ssrel  4456  ssrel2  4458  ssrelrel  4468  funfvima2  5419  tfrlem1  5954  tfrlemi1  5977  tfri3  5984  rdgon  6004  nneneq  6351  ac6sfi  6383  pitonn  6982  nnaddcl  8010  nnmulcl  8011  zaddcllempos  8339  zaddcllemneg  8341  peano5uzti  8405  uzind2  8409  fzind  8412  zindd  8415  uzaddcl  8625  frec2uzltd  9353  iseqss  9390  iseqfveq2  9392  iseqshft2  9396  monoord  9399  iseqsplit  9402  iseqcaopr3  9404  iseqid3s  9410  iseqhomo  9412  iseqz  9413  expivallem  9421  expcllem  9431  expap0  9450  mulexp  9459  expadd  9462  expmul  9465  leexp2r  9474  leexp1a  9475  bernneq  9537  facdiv  9606  facwordi  9608  faclbnd  9609  faclbnd6  9612  cjexp  9721  resqrexlemover  9837  resqrexlemdecn  9839  resqrexlemlo  9840  resqrexlemcalc3  9843  absexp  9906  dvdsfac  10172  nn0seqcvgd  10263  ialginv  10269  ialgcvga  10273  ialgfx  10274
  Copyright terms: Public domain W3C validator