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  847  minimp  1623  cbv1v  2341  cbv1  2407  ralimdva  3150  reuss2  4280  ssrel  5740  ssrel2  5742  ssrelrel  5753  funfvima2  7187  isofrlem  7296  dfwe2  7729  tfindsg  7813  tfinds2  7816  tfinds3  7817  trom  7827  findsg  7849  finds2  7850  xpord3inddlem  8106  fpr3g  8237  wfr3g  8271  tfrlem1  8317  tfr3  8340  tz7.48lem  8382  oaordi  8483  oeordi  8525  nnaordi  8556  nnawordi  8559  naddssim  8623  naddoa  8640  nneneq  9142  ac6sfi  9196  fodomfi  9224  domunfican  9234  fodomfiOLD  9242  finsschain  9271  marypha1lem  9348  inf3lem2  9550  inf3lem5  9553  cantnfval2  9590  cantnflt  9593  cantnfp1lem3  9601  cnfcom  9621  ttrclss  9641  ttrclselem2  9647  frr3g  9680  dfac12lem3  10068  ackbij1lem16  10156  sornom  10199  infpssrlem4  10228  fin23lem34  10268  fin23lem36  10270  isf32lem1  10275  isf32lem2  10276  zorn2lem4  10421  zorn2lem5  10422  zorn2lem6  10423  zorn2lem7  10424  ttukeylem5  10435  pwfseqlem3  10583  wunfi  10644  grudomon  10740  prlem934  10956  sup2  12110  nnindd  12177  nnaddcl  12180  nnmulcl  12181  nnne0  12191  peano5uzi  12593  uzind2  12597  nn0indd  12601  fzind  12602  zindd  12605  fzindd  12606  uzaddcl  12829  uzwo  12836  om2uzlti  13885  seqcaopr3  13972  seqf1olem2a  13975  seqf1o  13978  ser1const  13993  expcllem  14007  expeq0  14027  mulexp  14036  expadd  14039  expmul  14042  expmordi  14102  leexp2r  14109  leexp1a  14110  bernneq  14164  modexp  14173  facdiv  14222  facwordi  14224  faclbnd  14225  faclbnd4lem4  14231  hashgadd  14312  hashmap  14370  hashf1lem2  14391  hashf1  14392  seqcoll  14399  cshweqrep  14756  relexpsucnnl  14965  relexpcnv  14970  relexpnndm  14976  relexpaddnn  14986  rlimsqzlem  15584  lo1le  15587  iseraltlem2  15618  fsum2d  15706  modfsummod  15729  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  binom  15765  climcndslem1  15784  climcndslem2  15785  cvgrat  15818  clim2prod  15823  prodfn0  15829  prodfrec  15830  ntrivcvgfvn0  15834  fprodabs  15909  fprod2d  15916  binomfallfac  15976  bpolycl  15987  fprodefsum  16030  demoivreALT  16138  ruclem8  16174  ruclem9  16175  dvdsfac  16265  bitsinv1  16381  sadcadd  16397  sadadd2  16399  saddisjlem  16403  smuval2  16421  smupvallem  16422  smu01lem  16424  smupval  16427  smueqlem  16429  smumullem  16431  rplpwr  16497  nn0seqcvgd  16509  seq1st  16510  alginv  16514  algcvga  16518  algfx  16519  prmdvdsexp  16654  prmfac1  16659  eulerthlem2  16721  pcmpt  16832  pcfac  16839  prmpwdvds  16844  prmreclem4  16859  vdwlem10  16930  ramcl  16969  mreexexd  17583  frmdgsum  18799  mulgnnass  19051  mhmmulg  19057  gsumwrev  19307  gsmsymgrfix  19369  gsmsymgreq  19373  efginvrel2  19668  efgsrel  19675  gsum2dlem2  19912  ablfac1eulem  20015  pgpfac  20027  gsumle  20086  srgmulgass  20164  srgpcomp  20165  srgbinom  20178  lmodvsmmulgdi  20860  cnfldexp  21371  ofldchr  21543  assamulgscm  21869  mplcoe1  22004  mplcoe3  22005  mplcoe5  22007  mptcoe1fsupp  22168  coe1fzgsumdlem  22259  coe1fzgsumd  22260  gsummoncoe1  22264  evl1gsumdlem  22312  evl1gsumd  22313  mdetunilem9  22576  mptcoe1matfsupp  22758  mp2pm2mplem4  22765  chpdmat  22797  tgcl  22925  fiuncmp  23360  2ndcsep  23415  1stcelcls  23417  ptcmpfi  23769  tmdgsum  24051  fsumcn  24829  caubl  25276  caublcls  25277  ovolunlem1a  25465  ovolfiniun  25470  volfiniun  25516  voliunlem1  25519  volsuplem  25524  volsup  25525  dyadmax  25567  itgfsum  25796  dvnadd  25899  cpnord  25905  dvnfre  25924  dvmptfsum  25947  ply1divex  26110  fta1g  26143  plyco  26214  dgrcolem1  26247  dgrco  26249  dvnply2  26263  plydivex  26273  aaliou3lem2  26319  dvntaylp  26347  taylthlem1  26349  cxpmul2  26666  jensen  26967  ftalem2  27052  bcmono  27256  bposlem5  27267  lgsquad2lem2  27364  dchrisumlem1  27468  dchrisum0flb  27489  pntpbnd1  27565  pntlemf  27584  qabvle  27604  qabvexp  27605  ostthlem2  27607  ostth2lem2  27613  nosupbnd1lem5  27692  noinfbnd1lem5  27707  precsexlem8  28222  precsexlem9  28223  om2noseqrdg  28312  n0addscl  28352  n0mulscl  28353  eucliddivs  28384  peano5uzs  28412  expscllem  28438  expadds  28443  expsne0  28444  expsgt0  28445  pw2cut  28468  pw2cut2  28470  rusgrnumwwlk  30063  eupth2lems  30325  eupth2  30326  ipasslem1  30918  mdslmd1lem1  32412  mdslmd1lem2  32413  iuninc  32646  ssrelf  32704  nn0min  32911  nexple  32935  gsumwun  33169  gsumvsca1  33319  gsumvsca2  33320  domnprodn0  33368  unitprodclb  33481  1arithufdlem3  33638  cmppcmp  34035  esumfzf  34246  sseqp1  34572  rrvsum  34631  signstfvc  34751  bnj1174  35178  lfuhgr2  35332  subfacp1lem6  35398  mrsubvrs  35735  bccolsum  35952  iprodefisumlem  35953  faclimlem1  35956  onsuct0  36654  findfvcl  36665  poimirlem28  37893  sdclem2  37987  seqpo  37992  incsequz  37993  mettrifi  38002  heiborlem4  38059  bfplem1  38067  pclfinclN  40320  uzindd  42341  indstrd  42557  nnaddcom  42632  nnadddir  42634  nnmulcom  42636  sn-sup2  42855  incssnn0  43062  mzpexpmpt  43096  pell14qrexpclnn0  43217  monotuz  43292  rmxypos  43298  jm2.17a  43311  jm2.17b  43312  rmygeid  43315  jm2.18  43339  jm2.19lem3  43342  jm2.15nn0  43354  jm2.16nn0  43355  dfac11  43413  pwslnm  43445  hbtlem5  43479  cnsrexpcl  43516  cantnfresb  43675  onmcl  43682  naddonnn  43746  relexpxpnnidm  44053  relexpiidm  44054  relexpss1d  44055  iunrelexpmin1  44058  relexpmulnn  44059  iunrelexpmin2  44062  relexp0a  44066  trclimalb2  44076  dvgrat  44662  relpfrlem  45303  trfr  45312  lmodvsmdi  48733  tfis2d  50033