Theorem a2d 29

Description: Deduction distributing an embedded antecedent. Deduction form of ax-2 7. (Contributed by NM, 23-Jun-1994.)

Hypothesis

Ref	Expression
a2d.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
a2d	⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

Proof of Theorem a2d

Step	Hyp	Ref	Expression
1		a2d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2		ax-2 7	. 2 ⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
3	1, 2	syl 17	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

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  43  imim2d  57  imim3i  64  loowoz  112  animpimp2impd  843  minimp  1624  cbv1v  2334  cbv1  2403  ralimdva  3109  reuss2  4250  ssrel  5694  ssrelOLD  5695  ssrel2  5697  ssrelrel  5708  funfvima2  7116  isofrlem  7220  dfwe2  7633  tfindsg  7716  tfinds2  7719  tfinds3  7720  trom  7730  findsg  7755  finds2  7756  fpr3g  8110  wfr3g  8147  tfrlem1  8216  tfr3  8239  tz7.48lem  8281  oaordi  8386  oeordi  8427  nnaordi  8458  nnawordi  8461  nneneq  9001  nneneqOLD  9013  ac6sfi  9067  domunfican  9096  fodomfi  9101  finsschain  9135  marypha1lem  9201  inf3lem2  9396  inf3lem5  9399  cantnfval2  9436  cantnflt  9439  cantnfp1lem3  9447  cnfcom  9467  ttrclss  9487  ttrclselem2  9493  frr3g  9523  dfac12lem3  9910  ackbij1lem16  10000  sornom  10042  infpssrlem4  10071  fin23lem34  10111  fin23lem36  10113  isf32lem1  10118  isf32lem2  10119  zorn2lem4  10264  zorn2lem5  10265  zorn2lem6  10266  zorn2lem7  10267  ttukeylem5  10278  pwfseqlem3  10425  wunfi  10486  grudomon  10582  prlem934  10798  sup2  11940  nnindd  12002  nnaddcl  12005  nnmulcl  12006  nnne0  12016  peano5uzi  12418  uzind2  12422  nn0indd  12426  fzind  12427  zindd  12430  fzindd  12431  uzaddcl  12653  uzwo  12660  om2uzlti  13679  seqcaopr3  13767  seqf1olem2a  13770  seqf1o  13773  ser1const  13788  expcllem  13802  expeq0  13822  mulexp  13831  expadd  13834  expmul  13837  expmordi  13894  leexp2r  13901  leexp1a  13902  bernneq  13953  modexp  13962  facdiv  14010  facwordi  14012  faclbnd  14013  faclbnd4lem4  14019  hashgadd  14101  hashmap  14159  hashf1lem2  14179  hashf1  14180  seqcoll  14187  cshweqrep  14543  relexpsucnnl  14750  relexpcnv  14755  relexpnndm  14761  relexpaddnn  14771  rlimsqzlem  15369  lo1le  15372  iseraltlem2  15403  fsum2d  15492  modfsummod  15515  fsumabs  15522  fsumrlim  15532  fsumo1  15533  fsumiun  15542  binom  15551  climcndslem1  15570  climcndslem2  15571  cvgrat  15604  clim2prod  15609  prodfn0  15615  prodfrec  15616  ntrivcvgfvn0  15620  fprodabs  15693  fprod2d  15700  binomfallfac  15760  bpolycl  15771  fprodefsum  15813  demoivreALT  15919  ruclem8  15955  ruclem9  15956  dvdsfac  16044  bitsinv1  16158  sadcadd  16174  sadadd2  16176  saddisjlem  16180  smuval2  16198  smupvallem  16199  smu01lem  16201  smupval  16204  smueqlem  16206  smumullem  16208  gcdmultipleOLD  16269  rplpwr  16276  nn0seqcvgd  16284  seq1st  16285  alginv  16289  algcvga  16293  algfx  16294  prmdvdsexp  16429  prmfac1  16435  eulerthlem2  16492  pcmpt  16602  pcfac  16609  prmpwdvds  16614  prmreclem4  16629  vdwlem10  16700  ramcl  16739  mreexexd  17366  frmdgsum  18510  mulgnnass  18747  mhmmulg  18753  gsumwrev  18982  gsmsymgrfix  19045  gsmsymgreq  19049  efginvrel2  19342  efgsrel  19349  gsum2dlem2  19581  ablfac1eulem  19684  pgpfac  19696  srgmulgass  19776  srgpcomp  19777  srgbinom  19790  lmodvsmmulgdi  20167  cnfldexp  20640  assamulgscm  21114  mplcoe1  21247  mplcoe3  21248  mplcoe5  21250  mptcoe1fsupp  21395  coe1fzgsumdlem  21481  coe1fzgsumd  21482  gsummoncoe1  21484  evl1gsumdlem  21531  evl1gsumd  21532  mdetunilem9  21778  mptcoe1matfsupp  21960  mp2pm2mplem4  21967  chpdmat  21999  tgcl  22128  fiuncmp  22564  2ndcsep  22619  1stcelcls  22621  ptcmpfi  22973  tmdgsum  23255  fsumcn  24042  caubl  24481  caublcls  24482  ovolunlem1a  24669  ovolfiniun  24674  volfiniun  24720  voliunlem1  24723  volsuplem  24728  volsup  24729  dyadmax  24771  itgfsum  25000  dvnadd  25102  cpnord  25108  dvnfre  25125  dvmptfsum  25148  ply1divex  25310  fta1g  25341  plyco  25411  dgrcolem1  25443  dgrco  25445  dvnply2  25456  plydivex  25466  aaliou3lem2  25512  dvntaylp  25539  taylthlem1  25541  cxpmul2  25853  jensen  26147  ftalem2  26232  bcmono  26434  bposlem5  26445  lgsquad2lem2  26542  dchrisumlem1  26646  dchrisum0flb  26667  pntpbnd1  26743  pntlemf  26762  qabvle  26782  qabvexp  26783  ostthlem2  26785  ostth2lem2  26791  rusgrnumwwlk  28349  eupth2lems  28611  eupth2  28612  ipasslem1  29202  mdslmd1lem1  30696  mdslmd1lem2  30697  iuninc  30909  ssrelf  30964  nn0min  31143  gsumle  31359  gsumvsca1  31488  gsumvsca2  31489  ofldchr  31522  cmppcmp  31817  nexple  31986  esumfzf  32046  sseqp1  32371  rrvsum  32430  signstfvc  32562  bnj1174  32992  lfuhgr2  33089  subfacp1lem6  33156  mrsubvrs  33493  bccolsum  33714  iprodefisumlem  33715  faclimlem1  33718  naddssim  33846  nosupbnd1lem5  33924  noinfbnd1lem5  33939  onsuct0  34639  findfvcl  34650  poimirlem28  35814  sdclem2  35909  seqpo  35914  incsequz  35915  mettrifi  35924  heiborlem4  35981  bfplem1  35989  pclfinclN  37971  uzindd  39992  nnaddcom  40305  nnadddir  40307  nnmulcom  40309  sn-sup2  40446  incssnn0  40540  mzpexpmpt  40574  pell14qrexpclnn0  40695  monotuz  40770  rmxypos  40776  jm2.17a  40789  jm2.17b  40790  rmygeid  40793  jm2.18  40817  jm2.19lem3  40820  jm2.15nn0  40832  jm2.16nn0  40833  dfac11  40894  pwslnm  40926  hbtlem5  40960  cnsrexpcl  40997  relexpxpnnidm  41318  relexpiidm  41319  relexpss1d  41320  iunrelexpmin1  41323  relexpmulnn  41324  iunrelexpmin2  41327  relexp0a  41331  trclimalb2  41341  dvgrat  41937  lmodvsmdi  45729  tfis2d  46397