Theorem impd 414

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 410	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  impcomd  415  imp32  422  imp4b  425  imp4c  427  imp4d  428  imp5d  443  imp5g  445  pm3.31  453  expimpd  457  expl  461  ancomsd  469  syland  612  3expib  1134  ax13lem1  2404  equs5  2490  rsp2  3278  moi  3680  reu6  3688  elpwunsn  4642  opthpr  4808  preqsnd  4816  opthprneg  4822  3elpr2eq  4863  invdisj  5085  snopeqop  5474  solin  5580  sotr2  5587  wefrc  5639  relop  5820  elinxp  6003  reuop  6276  dfpo2  6279  tz7.7  6368  ordtr2  6387  funopsnOLD  7127  tpres  7181  funfvima  7210  isomin  7317  sorpsscmpl  7713  peano5  7870  resf1ext2b  7912  f1oweALT  7949  poxp  8103  soxp  8104  tfr3  8365  tz7.48-1  8409  omordi  8530  odi  8543  omass  8544  oen0  8551  nndi  8588  nnmass  8589  nnmordi  8596  eroveu  8789  ssfi  9137  findcard3  9223  fiint  9267  suplub  9403  hartogs  9489  card2on  9499  unxpwdom2  9533  inf3lem2  9581  ttrclselem2  9678  epfrs  9683  tcel  9695  frr3g  9711  dfac2b  10084  infpssr  10262  isf32lem9  10315  axdc3lem4  10407  axcclem  10411  zorn2lem7  10456  ttukeylem6  10468  brdom6disj  10486  ondomon  10517  inar1  10730  gruen  10767  indpi  10862  nqereu  10884  genpn0  10958  distrlem1pr  10980  distrlem5pr  10982  ltexprlem1  10991  reclem4pr  11005  addsrmo  11028  mulsrmo  11029  supsrlem  11066  lelttr  11270  ltlen  11281  mulgt1OLD  12047  fzind  12668  xrlelttr  13155  xnn0xaddcl  13235  fzen  13543  bernneq  14239  swrdswrdlem  14714  repsdf2  14788  limsupbnd2  15493  mulcn2  15606  prodmolem2  15948  dvdsmod0  16275  lcmfunsnlem1  16654  divgcdcoprm0  16682  maxprmfct  16727  pceu  16865  dvdsprmpweqnn  16904  oddprmdvds  16922  infpnlem1  16929  prmgaplem6  17075  imasaddfnlem  17541  initoeu1  18027  termoeu1  18034  plelttr  18357  gsumval2a  18702  cycsubm  19226  symgfix2  19439  psgnunilem4  19520  lsmmod  19698  efgrelexlemb  19773  imasabl  19899  pgpfac1lem5  20104  rngqiprngimf1lem  21344  rngqiprngimfo  21351  nzerooringczr  21512  lindfrn  21853  mat1dimcrng  22517  dmatelnd  22536  mdetunilem7  22658  cpmatacl  22756  cpmatmcllem  22758  lmss  23338  hausnei2  23393  isnrm2  23398  isnrm3  23399  cmpsublem  23439  2ndcdisj  23496  txcnpi  23648  tx1stc  23690  fgcl  23918  ufileu  23959  fmfnfmlem4  23997  fmfnfm  23998  alexsubALTlem4  24090  alexsubALT  24091  tmdgsum2  24136  prdsxmslem2  24569  ovolicc2  25564  volfiniun  25589  dyadmax  25640  ellimc3  25921  dvlip2  26037  dvne0  26053  dvfsumlem2  26069  taylthlem2  26414  zabsle1  27337  2lgslem3  27445  2sqreulem3  27494  ltlesnd  27816  cutsun12  27860  mulsproplem9  28194  mulsprop  28200  bdayons  28346  n0ssoldg  28423  eucliddivs  28446  bdayfinbndlem1  28537  axcontlem4  29114  uhgr2edg  29355  ushgredgedg  29376  ushgredgedgloop  29378  nb3grprlem1  29527  rusgr1vtx  29735  wlkonl1iedg  29810  uhgrwkspthlem2  29900  usgr2wlkneq  29902  usgr2trlncl  29906  uspgrn2crct  29954  wspthsnonn0vne  30063  usgrwwlks2on  30104  umgrwwlks2on  30105  elwspths2on  30108  elwspths2onw  30109  clwlkclwwlkf1lem3  30154  erclwwlktr  30170  erclwwlkntr  30219  frgrnbnb  30441  frgr2wwlk1  30477  frrusgrord  30489  wlkl0  30515  isch3  31390  ocin  31445  shmodsi  31538  spansneleq  31719  stj  32384  atom1d  32502  atcvat2i  32536  chirredlem1  32539  chirredi  32543  mdsymlem3  32554  mdsymlem6  32557  ssdifidlprm  33606  bnj849  35184  fineqvinfep  35385  pconnconn  35545  cvmsss2  35588  cvmliftlem7  35605  satfv0  35672  satfv0fun  35685  satffunlem  35715  satffunlem1lem1  35716  satffunlem2lem1  35718  mclsind  35884  dfon2lem9  36103  dfon2  36104  cgrextend  36322  btwntriv2  36326  btwncomim  36327  btwnexch3  36334  funtransport  36345  ifscgr  36358  colinearxfr  36389  lineext  36390  fscgr  36394  outsideoftr  36443  trer  36640  finminlem  36642  fnessref  36681  fgmin  36694  axnulregtco  36804  bj-andnotim  36995  bj-alanim  37034  bj-axreprepsep  37524  bj-0int  37555  relowlssretop  37821  finorwe  37840  finxpsuclem  37855  wl-ax13lem1  37952  poimirlem29  38112  itg2addnclem3  38136  itg2addnc  38137  areacirc  38176  ismtybndlem  38269  heibor1lem  38272  iss2  38807  disjlem17  39365  membpartlem19  39377  prtlem17  39464  riotasvd  39544  lshpsmreu  39697  atnle  39905  cvratlem  40009  cvrat2  40017  3dim1  40055  2llnjN  40155  2lplnj  40208  linepsubN  40340  pmapsub  40356  paddasslem14  40421  pclfinN  40488  ispsubcl2N  40535  pclfinclN  40538  ldilval  40701  trlord  41157  cdlemk36  41501  dihlsscpre  41822  baerlem3lem2  42298  baerlem5alem2  42299  baerlem5blem2  42300  pellexlem5  43374  pellex  43376  pell1234qrmulcl  43396  pellfundex  43427  cantnfresb  43865  omabs2  43873  relexpmulnn  44249  clsk1indlem3  44583  19.41rg  45090  iunconnlem2  45474  relpmin  45492  or2expropbi  47592  fcoresf1  47627  euoreqb  47667  2reu8i  47671  dfatcolem  47813  f1oresf1o2  47849  nltle2tri  47871  imasetpreimafvbijlemf1  47974  iccpartnel  48008  ich2exprop  48041  ichreuopeq  48043  paireqne  48081  prprelprb  48087  reupr  48092  reuopreuprim  48096  nprmmul3  48099  fmtnofac2lem  48141  sfprmdvdsmersenne  48176  lighneallem3  48180  lighneallem4  48183  requad2  48209  bgoldbtbnd  48395  dfnbgr6  48443  isubgredg  48452  grimuhgr  48473  grimco  48475  uhgrimedgi  48476  isuspgrimlem  48481  clnbgrgrimlem  48519  grimedg  48521  gpgvtxedg0  48649  gpgvtxedg1  48650  gpgedg2ov  48652  gpgedg2iv  48653  pgnbgreunbgrlem1  48699  pgnbgreunbgrlem2lem1  48700  pgnbgreunbgrlem2lem2  48701  pgnbgreunbgrlem2lem3  48702  pgnbgreunbgrlem2  48703  pgnbgreunbgrlem3  48704  pgnbgreunbgrlem4  48705  pgnbgreunbgrlem5  48709  pgnbgreunbgrlem6  48710  pgnbgreunbgr  48711  upgrwlkupwlk  48726  ldepspr  49059  affinecomb1  49288  itsclc0  49357  aacllem  50386