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  842  minimp  1622  cbv1v  2356  cbv1  2422  ralimdva  3179  reuss2  4285  ssrel  5659  ssrel2  5661  ssrelrel  5671  funfvima2  6995  isofrlem  7095  dfwe2  7498  tfindsg  7577  tfinds2  7580  tfinds3  7581  ordom  7591  findsg  7611  finds2  7612  wfr3g  7955  tfrlem1  8014  tfr3  8037  tz7.48lem  8079  oaordi  8174  oeordi  8215  nnaordi  8246  nnawordi  8249  nneneq  8702  ac6sfi  8764  domunfican  8793  fodomfi  8799  finsschain  8833  marypha1lem  8899  inf3lem2  9094  inf3lem5  9097  cantnfval2  9134  cantnflt  9137  cantnfp1lem3  9145  cnfcom  9165  dfac12lem3  9573  ackbij1lem16  9659  sornom  9701  infpssrlem4  9730  fin23lem34  9770  fin23lem36  9772  isf32lem1  9777  isf32lem2  9778  zorn2lem4  9923  zorn2lem5  9924  zorn2lem6  9925  zorn2lem7  9926  ttukeylem5  9937  pwfseqlem3  10084  wunfi  10145  grudomon  10241  prlem934  10457  sup2  11599  nnindd  11660  nnaddcl  11663  nnmulcl  11664  nnne0  11674  peano5uzi  12074  uzind2  12078  nn0indd  12082  fzind  12083  zindd  12086  uzaddcl  12307  uzwo  12314  om2uzlti  13321  seqcaopr3  13408  seqf1olem2a  13411  seqf1o  13414  ser1const  13429  expcllem  13443  expeq0  13462  mulexp  13471  expadd  13474  expmul  13477  expmordi  13534  leexp2r  13541  leexp1a  13542  bernneq  13593  modexp  13602  facdiv  13650  facwordi  13652  faclbnd  13653  faclbnd4lem4  13659  hashgadd  13741  hashmap  13799  hashf1lem2  13817  hashf1  13818  seqcoll  13825  cshweqrep  14185  relexpsucnnl  14393  relexpcnv  14396  relexpnndm  14402  relexpaddnn  14412  rlimsqzlem  15007  lo1le  15010  iseraltlem2  15041  fsum2d  15128  modfsummod  15151  fsumabs  15158  fsumrlim  15168  fsumo1  15169  fsumiun  15178  binom  15187  climcndslem1  15206  climcndslem2  15207  cvgrat  15241  clim2prod  15246  prodfn0  15252  prodfrec  15253  ntrivcvgfvn0  15257  fprodabs  15330  fprod2d  15337  binomfallfac  15397  bpolycl  15408  fprodefsum  15450  demoivreALT  15556  ruclem8  15592  ruclem9  15593  dvdsfac  15678  bitsinv1  15793  sadcadd  15809  sadadd2  15811  saddisjlem  15815  smuval2  15833  smupvallem  15834  smu01lem  15836  smupval  15839  smueqlem  15841  smumullem  15843  gcdmultipleOLD  15902  rplpwr  15909  nn0seqcvgd  15916  seq1st  15917  alginv  15921  algcvga  15925  algfx  15926  prmdvdsexp  16061  prmfac1  16065  eulerthlem2  16121  pcmpt  16230  pcfac  16237  prmpwdvds  16242  prmreclem4  16257  vdwlem10  16328  ramcl  16367  mreexexd  16921  frmdgsum  18029  mulgnnass  18264  mhmmulg  18270  gsumwrev  18496  gsmsymgrfix  18558  gsmsymgreq  18562  efginvrel2  18855  efgsrel  18862  gsum2dlem2  19093  ablfac1eulem  19196  pgpfac  19208  srgmulgass  19283  srgpcomp  19284  srgbinom  19297  lmodvsmmulgdi  19671  assamulgscm  20132  mplcoe1  20248  mplcoe3  20249  mplcoe5  20251  mptcoe1fsupp  20385  coe1fzgsumdlem  20471  coe1fzgsumd  20472  gsummoncoe1  20474  evl1gsumdlem  20521  evl1gsumd  20522  cnfldexp  20580  mdetunilem9  21231  mptcoe1matfsupp  21412  mp2pm2mplem4  21419  chpdmat  21451  tgcl  21579  fiuncmp  22014  2ndcsep  22069  1stcelcls  22071  ptcmpfi  22423  tmdgsum  22705  fsumcn  23480  caubl  23913  caublcls  23914  ovolunlem1a  24099  ovolfiniun  24104  volfiniun  24150  voliunlem1  24153  volsuplem  24158  volsup  24159  dyadmax  24201  itgfsum  24429  dvnadd  24528  cpnord  24534  dvnfre  24551  dvmptfsum  24574  ply1divex  24732  fta1g  24763  plyco  24833  dgrcolem1  24865  dgrco  24867  dvnply2  24878  plydivex  24888  aaliou3lem2  24934  dvntaylp  24961  taylthlem1  24963  cxpmul2  25274  jensen  25568  ftalem2  25653  bcmono  25855  bposlem5  25866  lgsquad2lem2  25963  dchrisumlem1  26067  dchrisum0flb  26088  pntpbnd1  26164  pntlemf  26183  qabvle  26203  qabvexp  26204  ostthlem2  26206  ostth2lem2  26212  rusgrnumwwlk  27756  eupth2lems  28019  eupth2  28020  ipasslem1  28610  mdslmd1lem1  30104  mdslmd1lem2  30105  iuninc  30314  ssrelf  30368  nn0min  30538  gsumle  30727  gsumvsca1  30856  gsumvsca2  30857  ofldchr  30889  cmppcmp  31124  nexple  31270  esumfzf  31330  sseqp1  31655  rrvsum  31714  signstfvc  31846  bnj1174  32277  lfuhgr2  32367  subfacp1lem6  32434  mrsubvrs  32771  bccolsum  32973  iprodefisumlem  32974  faclimlem1  32977  trpredmintr  33072  frr3g  33123  fpr3g  33124  nosupbnd1lem5  33214  onsuct0  33791  findfvcl  33802  poimirlem28  34922  sdclem2  35019  seqpo  35024  incsequz  35025  mettrifi  35034  heiborlem4  35094  bfplem1  35102  pclfinclN  37088  nnaddcom  39168  nnadddir  39170  nnmulcom  39172  incssnn0  39315  mzpexpmpt  39349  pell14qrexpclnn0  39470  monotuz  39545  rmxypos  39551  jm2.17a  39564  jm2.17b  39565  rmygeid  39568  jm2.18  39592  jm2.19lem3  39595  jm2.15nn0  39607  jm2.16nn0  39608  dfac11  39669  pwslnm  39701  hbtlem5  39735  cnsrexpcl  39772  relexpxpnnidm  40055  relexpiidm  40056  relexpss1d  40057  iunrelexpmin1  40060  relexpmulnn  40061  iunrelexpmin2  40064  relexp0a  40068  trclimalb2  40078  dvgrat  40651  lmodvsmdi  44437  tfis2d  44790