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  111  minimp  1560  cbv1  2267  ralimdva  2962  reuss2  3907  ssrel  5207  ssrelOLD  5208  ssrel2  5210  ssrelrel  5220  funfvima2  6493  isofrlem  6590  dfwe2  6981  tfindsg  7060  tfinds2  7063  tfinds3  7064  ordom  7074  findsg  7093  finds2  7094  wfr3g  7413  tfrlem1  7472  tfr3  7495  tz7.48lem  7536  oaordi  7626  oeordi  7667  nnaordi  7698  nnawordi  7701  nneneq  8143  ac6sfi  8204  domunfican  8233  fodomfi  8239  finsschain  8273  marypha1lem  8339  inf3lem2  8526  inf3lem5  8529  cantnfval2  8566  cantnflt  8569  cantnfp1lem3  8577  cnfcom  8597  dfac12lem3  8967  ackbij1lem16  9057  sornom  9099  infpssrlem4  9128  fin23lem34  9168  fin23lem36  9170  isf32lem1  9175  isf32lem2  9176  zorn2lem4  9321  zorn2lem5  9322  zorn2lem6  9323  zorn2lem7  9324  ttukeylem5  9335  pwfseqlem3  9482  wunfi  9543  grudomon  9639  prlem934  9855  sup2  10979  nnaddcl  11042  nnmulcl  11043  peano5uzi  11466  uzind2  11470  nn0indd  11474  fzind  11475  zindd  11478  uzaddcl  11744  uzwo  11751  om2uzlti  12749  seqcl2  12819  seqfveq2  12823  seqshft2  12827  monoord  12831  seqsplit  12834  seqcaopr3  12836  seqf1olem2a  12839  seqf1o  12842  seqid2  12847  seqhomo  12848  ser1const  12857  expcllem  12871  expeq0  12890  mulexp  12899  expadd  12902  expmul  12905  leexp2r  12918  leexp1a  12919  bernneq  12990  modexp  12999  facdiv  13074  facwordi  13076  faclbnd  13077  faclbnd4lem4  13083  faclbnd6  13086  hashgadd  13166  hashmap  13222  hashf1lem2  13240  hashf1  13241  seqcoll  13248  cshweqrep  13567  relexpsucnnl  13772  relexpcnv  13775  relexpnndm  13781  relexpaddnn  13791  cjexp  13890  absexp  14044  rlimsqzlem  14379  lo1le  14382  iseraltlem2  14413  fsum2d  14502  modfsummod  14526  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  binom  14562  bcxmas  14567  climcndslem1  14581  climcndslem2  14582  cvgrat  14615  clim2prod  14620  prodfn0  14626  prodfrec  14627  ntrivcvgfvn0  14631  fprodabs  14704  fprod2d  14711  binomfallfac  14772  bpolycl  14783  fprodefsum  14825  demoivreALT  14931  ruclem8  14966  ruclem9  14967  dvdsfac  15048  bitsinv1  15164  sadcadd  15180  sadadd2  15182  saddisjlem  15186  smuval2  15204  smupvallem  15205  smu01lem  15207  smupval  15210  smueqlem  15212  smumullem  15214  gcdmultiple  15269  rplpwr  15276  nn0seqcvgd  15283  seq1st  15284  alginv  15288  algcvga  15292  algfx  15293  prmdvdsexp  15427  prmfac1  15431  eulerthlem2  15487  pcmpt  15596  pcfac  15603  prmpwdvds  15608  prmreclem4  15623  vdwlem10  15694  ramcl  15733  mreexexd  16308  mreexexdOLD  16309  frmdgsum  17399  mulgnnass  17576  mulgnnassOLD  17577  mhmmulg  17583  gsumwrev  17796  gsmsymgrfix  17848  gsmsymgreq  17852  sylow1lem1  18013  efginvrel2  18140  efgsrel  18147  gsum2dlem2  18370  ablfac1eulem  18471  pgpfac  18483  srgmulgass  18531  srgpcomp  18532  srgbinom  18545  lmodvsmmulgdi  18898  assamulgscm  19350  mplcoe1  19465  mplcoe3  19466  mplcoe5  19468  mptcoe1fsupp  19585  coe1fzgsumdlem  19671  coe1fzgsumd  19672  gsummoncoe1  19674  evl1gsumdlem  19720  evl1gsumd  19721  cnfldexp  19779  mdetunilem9  20426  mptcoe1matfsupp  20607  mp2pm2mplem4  20614  chpdmat  20646  tgcl  20773  fiuncmp  21207  2ndcsep  21262  1stcelcls  21264  ptcmpfi  21616  tmdmulg  21896  tmdgsum  21899  imasdsf1olem  22178  fsumcn  22673  caubl  23106  caublcls  23107  ovolunlem1a  23264  ovolfiniun  23269  ovolicc2lem3  23287  volfiniun  23315  voliunlem1  23318  volsuplem  23323  volsup  23324  dyadmax  23366  itgfsum  23593  dvnadd  23692  dvnres  23694  cpnord  23698  dvnfre  23715  dvmptfsum  23738  ply1divex  23896  fta1g  23927  plyco  23997  dgrcolem1  24029  dgrco  24031  dvnply2  24042  plydivex  24052  aaliou3lem2  24098  dvntaylp  24125  taylthlem1  24127  cxpmul2  24435  jensen  24715  ftalem2  24800  bcmono  25002  bposlem5  25013  lgsquad2lem2  25110  dchrisumlem1  25178  dchrisum0flb  25199  pntpbnd1  25275  pntlemf  25294  qabvle  25314  qabvexp  25315  ostthlem2  25317  ostth2lem2  25323  rusgrnumwwlk  26870  eupth2lems  27098  eupth2  27099  ipasslem1  27686  mdslmd1lem1  29184  mdslmd1lem2  29185  iuninc  29379  ssrelf  29425  nnindd  29566  nn0min  29567  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  ofldchr  29814  cmppcmp  29925  nexple  30071  esumfzf  30131  sseqp1  30457  rrvsum  30516  signstfvc  30651  bnj1174  31071  subfacp1lem6  31167  cvmliftlem7  31273  cvmliftlem10  31276  mrsubvrs  31419  bccolsum  31625  iprodefisumlem  31626  faclimlem1  31629  trpredmintr  31731  frr3g  31779  nosupbnd1lem5  31858  onsuct0  32440  findfvcl  32451  bj-imim2ALT  32538  bj-cbv1v  32729  poimirlem28  33437  sdclem2  33538  seqpo  33543  incsequz  33544  mettrifi  33553  heiborlem4  33613  bfplem1  33621  pclfinclN  35236  incssnn0  37274  mzpexpmpt  37308  pell14qrexpclnn0  37430  monotuz  37506  expmordi  37512  rmxypos  37514  jm2.17a  37527  jm2.17b  37528  rmygeid  37531  jm2.18  37555  jm2.19lem3  37558  jm2.15nn0  37570  jm2.16nn0  37571  dfac11  37632  pwslnm  37664  hbtlem5  37698  cnsrexpcl  37735  relexpxpnnidm  37995  relexpiidm  37996  relexpss1d  37997  iunrelexpmin1  38000  relexpmulnn  38001  iunrelexpmin2  38004  relexp0a  38008  trclimalb2  38018  dvgrat  38511  smonoord  41341  lmodvsmdi  42163  tfis2d  42427