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 7 . 2 ((𝜓 → (𝜒𝜃)) → ((𝜓𝜒) → (𝜓𝜃)))
31, 2syl 14 1 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mpdd  41  imim2d  54  imim3i  61  loowoz  102  animpimp2impd  548  cbv1  1722  ralimdaa  2498  reuss2  3356  finds2  4515  ssrel  4627  ssrel2  4629  ssrelrel  4639  funfvima2  5650  tfrlem1  6205  tfrlemi1  6229  tfr1onlemaccex  6245  tfrcllemaccex  6258  tfri3  6264  nneneq  6751  ac6sfi  6792  pitonn  7663  nnaddcl  8747  nnmulcl  8748  zaddcllempos  9098  zaddcllemneg  9100  peano5uzti  9166  uzind2  9170  fzind  9173  zindd  9176  uzaddcl  9388  exfzdc  10024  frec2uzltd  10183  frecuzrdgg  10196  seq3val  10238  seqvalcd  10239  seq3clss  10247  monoord  10256  seq3caopr3  10261  seq3f1olemp  10282  seq3id3  10287  seq3homo  10290  seq3z  10291  ser3ge0  10297  exp3vallem  10301  expcllem  10311  expap0  10330  mulexp  10339  expadd  10342  expmul  10345  leexp2r  10354  leexp1a  10355  bernneq  10419  facdiv  10491  facwordi  10493  faclbnd  10494  faclbnd6  10497  omgadd  10555  seq3coll  10592  cjexp  10672  resqrexlemover  10789  resqrexlemdecn  10791  resqrexlemlo  10792  resqrexlemcalc3  10795  absexp  10858  fsum2d  11211  modfsummod  11234  fsumabs  11241  fsumiun  11253  binom  11260  bcxmas  11265  cvgratnnlemnexp  11300  cvgratnnlemmn  11301  clim2prod  11315  prodfap0  11321  prodfrecap  11322  demoivreALT  11487  dvdsfac  11565  gcdmultiple  11715  rplpwr  11722  nn0seqcvgd  11729  alginv  11735  algcvga  11739  algfx  11740  prmdvdsexp  11833  prmfac1  11837  ennnfoneleminc  11931  ennnfonelemkh  11932  ennnfonelemhf1o  11933  ennnfonelemhom  11935  tgcl  12243  nninfalllemn  13216  nninfsellemdc  13220
  Copyright terms: Public domain W3C validator