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  42  imim2d  55  imim3i  62  loowoz  110  minimp  1551  cbv1  2255  ralimdva  2945  reuss2  3866  ssrel  5130  ssrelOLD  5131  ssrel2  5133  ssrelrel  5143  funfvima2  6397  isofrlem  6490  dfwe2  6873  tfindsg  6952  tfinds2  6955  tfinds3  6956  ordom  6966  findsg  6985  finds2  6986  wfr3g  7300  tfrlem1  7359  tfr3  7382  tz7.48lem  7423  oaordi  7513  oeordi  7554  nnaordi  7585  nnawordi  7588  nneneq  8028  ac6sfi  8089  domunfican  8118  fodomfi  8124  finsschain  8156  marypha1lem  8222  inf3lem2  8409  inf3lem5  8412  cantnfval2  8449  cantnflt  8452  cantnfp1lem3  8460  cnfcom  8480  dfac12lem3  8850  ackbij1lem16  8940  sornom  8982  infpssrlem4  9011  fin23lem34  9051  fin23lem36  9053  isf32lem1  9058  isf32lem2  9059  zorn2lem4  9204  zorn2lem5  9205  zorn2lem6  9206  zorn2lem7  9207  ttukeylem5  9218  pwfseqlem3  9361  wunfi  9422  grudomon  9518  prlem934  9734  sup2  10858  nnaddcl  10919  nnmulcl  10920  peano5uzi  11342  uzind2  11346  nn0indd  11350  fzind  11351  zindd  11354  uzaddcl  11620  uzwo  11627  om2uzlti  12611  seqcl2  12681  seqfveq2  12685  seqshft2  12689  monoord  12693  seqsplit  12696  seqcaopr3  12698  seqf1olem2a  12701  seqf1o  12704  seqid2  12709  seqhomo  12710  ser1const  12719  expcllem  12733  expeq0  12752  mulexp  12761  expadd  12764  expmul  12767  leexp2r  12780  leexp1a  12781  bernneq  12852  modexp  12861  facdiv  12936  facwordi  12938  faclbnd  12939  faclbnd4lem4  12945  faclbnd6  12948  hashgadd  13027  hashmap  13082  hashf1lem2  13097  hashf1  13098  seqcoll  13105  cshweqrep  13418  relexpsucnnl  13620  relexpcnv  13623  relexpnndm  13629  relexpaddnn  13639  cjexp  13738  absexp  13892  rlimsqzlem  14227  lo1le  14230  iseraltlem2  14261  fsum2d  14344  modfsummod  14367  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  binom  14401  bcxmas  14406  climcndslem1  14420  climcndslem2  14421  cvgrat  14454  clim2prod  14459  prodfn0  14465  prodfrec  14466  ntrivcvgfvn0  14470  fprodabs  14543  fprod2d  14550  binomfallfac  14611  bpolycl  14622  fprodefsum  14664  demoivreALT  14770  ruclem8  14805  ruclem9  14806  dvdsfac  14886  bitsinv1  15002  sadcadd  15018  sadadd2  15020  saddisjlem  15024  smuval2  15042  smupvallem  15043  smu01lem  15045  smupval  15048  smueqlem  15050  smumullem  15052  gcdmultiple  15107  rplpwr  15114  nn0seqcvgd  15121  seq1st  15122  alginv  15126  algcvga  15130  algfx  15131  prmdvdsexp  15265  prmfac1  15269  eulerthlem2  15325  pcmpt  15434  pcfac  15441  prmpwdvds  15446  prmreclem4  15461  vdwlem10  15532  ramcl  15571  mreexexd  16131  mreexexdOLD  16132  frmdgsum  17222  mulgnnass  17399  mulgnnassOLD  17400  mhmmulg  17406  gsumwrev  17619  gsmsymgrfix  17671  gsmsymgreq  17675  sylow1lem1  17836  efginvrel2  17963  efgsrel  17970  gsum2dlem2  18193  ablfac1eulem  18294  pgpfac  18306  srgmulgass  18354  srgpcomp  18355  srgbinom  18368  lmodvsmmulgdi  18721  assamulgscm  19171  mplcoe1  19286  mplcoe3  19287  mplcoe5  19289  mptcoe1fsupp  19406  coe1fzgsumdlem  19492  coe1fzgsumd  19493  gsummoncoe1  19495  evl1gsumdlem  19541  evl1gsumd  19542  cnfldexp  19598  mdetunilem9  20245  mptcoe1matfsupp  20426  mp2pm2mplem4  20433  chpdmat  20465  tgcl  20584  fiuncmp  21017  2ndcsep  21072  1stcelcls  21074  ptcmpfi  21426  tmdmulg  21706  tmdgsum  21709  imasdsf1olem  21988  fsumcn  22481  caubl  22914  caublcls  22915  ovolunlem1a  23071  ovolfiniun  23076  ovolicc2lem3  23094  volfiniun  23122  voliunlem1  23125  volsuplem  23130  volsup  23131  dyadmax  23172  itgfsum  23399  dvnadd  23498  dvnres  23500  cpnord  23504  dvnfre  23521  dvmptfsum  23542  ply1divex  23700  fta1g  23731  plyco  23801  dgrcolem1  23833  dgrco  23835  dvnply2  23846  plydivex  23856  aaliou3lem2  23902  dvntaylp  23929  taylthlem1  23931  cxpmul2  24235  jensen  24515  ftalem2  24600  bcmono  24802  bposlem5  24813  lgsquad2lem2  24910  dchrisumlem1  24978  dchrisum0flb  24999  pntpbnd1  25075  pntlemf  25094  qabvle  25114  qabvexp  25115  ostthlem2  25117  ostth2lem2  25123  rusgranumwlk  26484  eupath2  26507  ipasslem1  27070  mdslmd1lem1  28568  mdslmd1lem2  28569  iuninc  28761  ssrelf  28805  nnindd  28953  nn0min  28954  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  ofldchr  29145  cmppcmp  29253  nexple  29399  esumfzf  29458  sseqp1  29784  rrvsum  29843  signstfvc  29977  bnj1174  30325  subfacp1lem6  30421  cvmliftlem7  30527  cvmliftlem10  30530  mrsubvrs  30673  bccolsum  30878  iprodefisumlem  30879  faclimlem1  30882  trpredmintr  30975  frr3g  31023  onsuct0  31610  findfvcl  31621  bj-imim2ALT  31708  bj-cbv1v  31916  poimirlem28  32607  sdclem2  32708  seqpo  32713  incsequz  32714  mettrifi  32723  heiborlem4  32783  bfplem1  32791  pclfinclN  34254  incssnn0  36292  mzpexpmpt  36326  pell14qrexpclnn0  36448  monotuz  36524  expmordi  36530  rmxypos  36532  jm2.17a  36545  jm2.17b  36546  rmygeid  36549  jm2.18  36573  jm2.19lem3  36576  jm2.15nn0  36588  jm2.16nn0  36589  dfac11  36650  pwslnm  36682  hbtlem5  36717  cnsrexpcl  36754  relexpxpnnidm  37014  relexpiidm  37015  relexpss1d  37016  iunrelexpmin1  37019  relexpmulnn  37020  iunrelexpmin2  37023  relexp0a  37027  trclimalb2  37037  dvgrat  37533  smonoord  39944  rusgrnumwwlk  41178  eupth2lems  41406  eupth2  41407  lmodvsmdi  41957  tfis2d  42225