Theorem impd 410

Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)

Hypothesis

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

Assertion

Ref	Expression
impd	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem impd

Step	Hyp	Ref	Expression
1		impd.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3l 89	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 406	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  impcomd  411  imp32  418  imp4b  421  imp4c  423  imp4d  424  imp5d  439  imp5g  441  pm3.31  449  expimpd  453  expl  457  ancomsd  465  syland  604  3expib  1123  ax13lem1  2379  equs5  2465  rsp2  3255  moi  3665  reu6  3673  sbciegftOLD  3767  elpwunsn  4629  opthpr  4795  preqsnd  4803  opthprneg  4809  3elpr2eq  4850  invdisj  5072  snopeqop  5454  solin  5559  sotr2  5566  wefrc  5618  relop  5799  elinxp  5978  reuop  6251  dfpo2  6254  tz7.7  6343  ordtr2  6362  funopsn  7095  tpres  7149  funfvima  7178  isomin  7285  sorpsscmpl  7681  peano5  7837  resf1ext2b  7879  f1oweALT  7918  poxp  8071  soxp  8072  tfr3  8331  tz7.48-1  8375  omordi  8494  odi  8507  omass  8508  oen0  8515  nndi  8552  nnmass  8553  nnmordi  8560  eroveu  8752  ssfi  9100  findcard3  9186  fiint  9230  suplub  9366  hartogs  9452  card2on  9462  unxpwdom2  9496  inf3lem2  9541  ttrclselem2  9638  epfrs  9643  tcel  9655  frr3g  9671  dfac2b  10044  infpssr  10221  isf32lem9  10274  axdc3lem4  10366  axcclem  10370  zorn2lem7  10415  ttukeylem6  10427  brdom6disj  10445  ondomon  10476  inar1  10689  gruen  10726  indpi  10821  nqereu  10843  genpn0  10917  distrlem1pr  10939  distrlem5pr  10941  ltexprlem1  10950  reclem4pr  10964  addsrmo  10987  mulsrmo  10988  supsrlem  11025  lelttr  11227  ltlen  11238  mulgt1OLD  12005  fzind  12618  xrlelttr  13098  xnn0xaddcl  13178  fzen  13486  bernneq  14182  swrdswrdlem  14657  repsdf2  14731  limsupbnd2  15436  mulcn2  15549  prodmolem2  15891  dvdsmod0  16218  lcmfunsnlem1  16597  divgcdcoprm0  16625  maxprmfct  16670  pceu  16808  dvdsprmpweqnn  16847  oddprmdvds  16865  infpnlem1  16872  prmgaplem6  17018  imasaddfnlem  17483  initoeu1  17969  termoeu1  17976  plelttr  18299  gsumval2a  18644  cycsubm  19168  symgfix2  19382  psgnunilem4  19463  lsmmod  19641  efgrelexlemb  19716  imasabl  19842  pgpfac1lem5  20047  rngqiprngimf1lem  21284  rngqiprngimfo  21291  nzerooringczr  21470  lindfrn  21811  mat1dimcrng  22452  dmatelnd  22471  mdetunilem7  22593  cpmatacl  22691  cpmatmcllem  22693  lmss  23273  hausnei2  23328  isnrm2  23333  isnrm3  23334  cmpsublem  23374  2ndcdisj  23431  txcnpi  23583  tx1stc  23625  fgcl  23853  ufileu  23894  fmfnfmlem4  23932  fmfnfm  23933  alexsubALTlem4  24025  alexsubALT  24026  tmdgsum2  24071  prdsxmslem2  24504  ovolicc2  25499  volfiniun  25524  dyadmax  25575  ellimc3  25856  dvlip2  25972  dvne0  25988  dvfsumlem2  26004  taylthlem2  26351  zabsle1  27273  2lgslem3  27381  2sqreulem3  27430  ltlesnd  27753  cutsun12  27796  mulsproplem9  28130  mulsprop  28136  bdayons  28282  n0ssoldg  28359  eucliddivs  28382  bdayfinbndlem1  28473  axcontlem4  29050  uhgr2edg  29291  ushgredgedg  29312  ushgredgedgloop  29314  nb3grprlem1  29463  rusgr1vtx  29672  wlkonl1iedg  29747  uhgrwkspthlem2  29837  usgr2wlkneq  29839  usgr2trlncl  29843  uspgrn2crct  29891  wspthsnonn0vne  30000  usgrwwlks2on  30041  umgrwwlks2on  30042  elwspths2on  30045  elwspths2onw  30046  clwlkclwwlkf1lem3  30091  erclwwlktr  30107  erclwwlkntr  30156  frgrnbnb  30378  frgr2wwlk1  30414  frrusgrord  30426  wlkl0  30452  isch3  31327  ocin  31382  shmodsi  31475  spansneleq  31656  stj  32321  atom1d  32439  atcvat2i  32473  chirredlem1  32476  chirredi  32480  mdsymlem3  32491  mdsymlem6  32494  ssdifidlprm  33533  bnj849  35083  fineqvinfep  35285  pconnconn  35429  cvmsss2  35472  cvmliftlem7  35489  satfv0  35556  satfv0fun  35569  satffunlem  35599  satffunlem1lem1  35600  satffunlem2lem1  35602  mclsind  35768  dfon2lem9  35987  dfon2  35988  cgrextend  36206  btwntriv2  36210  btwncomim  36211  btwnexch3  36218  funtransport  36229  ifscgr  36242  colinearxfr  36273  lineext  36274  fscgr  36278  outsideoftr  36327  trer  36514  finminlem  36516  fnessref  36555  fgmin  36568  axnulregtco  36678  bj-andnotim  36869  bj-alanim  36908  bj-axreprepsep  37398  bj-0int  37429  relowlssretop  37693  finorwe  37712  finxpsuclem  37727  wl-ax13lem1  37824  poimirlem29  37984  itg2addnclem3  38008  itg2addnc  38009  areacirc  38048  ismtybndlem  38141  heibor1lem  38144  iss2  38679  disjlem17  39237  membpartlem19  39249  prtlem17  39336  riotasvd  39416  lshpsmreu  39569  atnle  39777  cvratlem  39881  cvrat2  39889  3dim1  39927  2llnjN  40027  2lplnj  40080  linepsubN  40212  pmapsub  40228  paddasslem14  40293  pclfinN  40360  ispsubcl2N  40407  pclfinclN  40410  ldilval  40573  trlord  41029  cdlemk36  41373  dihlsscpre  41694  baerlem3lem2  42170  baerlem5alem2  42171  baerlem5blem2  42172  pellexlem5  43279  pellex  43281  pell1234qrmulcl  43301  pellfundex  43332  cantnfresb  43770  omabs2  43778  relexpmulnn  44154  clsk1indlem3  44488  19.41rg  44995  iunconnlem2  45379  relpmin  45397  or2expropbi  47494  fcoresf1  47529  euoreqb  47569  2reu8i  47573  dfatcolem  47715  f1oresf1o2  47751  nltle2tri  47773  imasetpreimafvbijlemf1  47876  iccpartnel  47910  ich2exprop  47943  ichreuopeq  47945  paireqne  47983  prprelprb  47989  reupr  47994  reuopreuprim  47998  nprmmul3  48001  fmtnofac2lem  48043  sfprmdvdsmersenne  48078  lighneallem3  48082  lighneallem4  48085  requad2  48111  bgoldbtbnd  48297  dfnbgr6  48345  isubgredg  48354  grimuhgr  48375  grimco  48377  uhgrimedgi  48378  isuspgrimlem  48383  clnbgrgrimlem  48421  grimedg  48423  gpgvtxedg0  48551  gpgvtxedg1  48552  gpgedg2ov  48554  gpgedg2iv  48555  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem2  48605  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5  48611  pgnbgreunbgrlem6  48612  pgnbgreunbgr  48613  upgrwlkupwlk  48628  ldepspr  48961  affinecomb1  49190  itsclc0  49259  aacllem  50288