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  603  3expib  1122  ax13lem1  2372  equs5  2458  rsp2  3254  moi  3689  reu6  3697  sbciegftOLD  3791  elpwunsn  4648  opthpr  4815  preqsnd  4823  opthprneg  4829  3elpr2eq  4870  invdisj  5093  snopeqop  5466  solin  5573  sotr2  5580  wefrc  5632  relop  5814  elinxp  5990  reuop  6266  dfpo2  6269  tz7.7  6358  ordtr2  6377  funopsn  7120  tpres  7175  funfvima  7204  isomin  7312  sorpsscmpl  7710  peano5  7869  resf1ext2b  7911  f1oweALT  7951  poxp  8107  soxp  8108  tfr3  8367  tz7.48-1  8411  omordi  8530  odi  8543  omass  8544  oen0  8550  nndi  8587  nnmass  8588  nnmordi  8595  eroveu  8785  ssfi  9137  findcard3  9229  findcard3OLD  9230  fiint  9277  fiintOLD  9278  suplub  9411  hartogs  9497  card2on  9507  unxpwdom2  9541  inf3lem2  9582  ttrclselem2  9679  epfrs  9684  tcel  9698  frr3g  9709  dfac2b  10084  infpssr  10261  isf32lem9  10314  axdc3lem4  10406  axcclem  10410  zorn2lem7  10455  ttukeylem6  10467  brdom6disj  10485  ondomon  10516  inar1  10728  gruen  10765  indpi  10860  nqereu  10882  genpn0  10956  distrlem1pr  10978  distrlem5pr  10980  ltexprlem1  10989  reclem4pr  11003  addsrmo  11026  mulsrmo  11027  supsrlem  11064  lelttr  11264  ltlen  11275  mulgt1OLD  12041  fzind  12632  xrlelttr  13116  xnn0xaddcl  13195  fzen  13502  bernneq  14194  swrdswrdlem  14669  repsdf2  14743  limsupbnd2  15449  mulcn2  15562  prodmolem2  15901  dvdsmod0  16228  lcmfunsnlem1  16607  divgcdcoprm0  16635  maxprmfct  16679  pceu  16817  dvdsprmpweqnn  16856  oddprmdvds  16874  infpnlem1  16881  prmgaplem6  17027  imasaddfnlem  17491  initoeu1  17973  termoeu1  17980  plelttr  18303  gsumval2a  18612  cycsubm  19134  symgfix2  19346  psgnunilem4  19427  lsmmod  19605  efgrelexlemb  19680  imasabl  19806  pgpfac1lem5  20011  rngqiprngimf1lem  21204  rngqiprngimfo  21211  nzerooringczr  21390  lindfrn  21730  mat1dimcrng  22364  dmatelnd  22383  mdetunilem7  22505  cpmatacl  22603  cpmatmcllem  22605  lmss  23185  hausnei2  23240  isnrm2  23245  isnrm3  23246  cmpsublem  23286  2ndcdisj  23343  txcnpi  23495  tx1stc  23537  fgcl  23765  ufileu  23806  fmfnfmlem4  23844  fmfnfm  23845  alexsubALTlem4  23937  alexsubALT  23938  tmdgsum2  23983  prdsxmslem2  24417  ovolicc2  25423  volfiniun  25448  dyadmax  25499  ellimc3  25780  dvlip2  25900  dvne0  25916  dvfsumlem2  25933  taylthlem2  26282  zabsle1  27207  2lgslem3  27315  2sqreulem3  27364  sltlend  27683  scutun12  27722  mulsproplem9  28027  mulsprop  28033  bdayon  28173  eucliddivs  28265  axcontlem4  28894  uhgr2edg  29135  ushgredgedg  29156  ushgredgedgloop  29158  nb3grprlem1  29307  rusgr1vtx  29516  wlkonl1iedg  29593  uhgrwkspthlem2  29684  usgr2wlkneq  29686  usgr2trlncl  29690  uspgrn2crct  29738  wspthsnonn0vne  29847  umgrwwlks2on  29887  elwspths2on  29890  clwlkclwwlkf1lem3  29935  erclwwlktr  29951  erclwwlkntr  30000  frgrnbnb  30222  frgr2wwlk1  30258  frrusgrord  30270  wlkl0  30296  isch3  31170  ocin  31225  shmodsi  31318  spansneleq  31499  stj  32164  atom1d  32282  atcvat2i  32316  chirredlem1  32319  chirredi  32323  mdsymlem3  32334  mdsymlem6  32337  ssdifidlprm  33429  bnj849  34915  pconnconn  35218  cvmsss2  35261  cvmliftlem7  35278  satfv0  35345  satfv0fun  35358  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  mclsind  35557  dfon2lem9  35779  dfon2  35780  cgrextend  35996  btwntriv2  36000  btwncomim  36001  btwnexch3  36008  funtransport  36019  ifscgr  36032  colinearxfr  36063  lineext  36064  fscgr  36068  outsideoftr  36117  trer  36304  finminlem  36306  fnessref  36345  fgmin  36358  bj-andnotim  36576  bj-alanim  36600  bj-0int  37089  relowlssretop  37351  finorwe  37370  finxpsuclem  37385  wl-ax13lem1  37482  poimirlem29  37643  itg2addnclem3  37667  itg2addnc  37668  areacirc  37707  ismtybndlem  37800  heibor1lem  37803  iss2  38326  disjlem17  38791  membpartlem19  38803  prtlem17  38869  riotasvd  38949  lshpsmreu  39102  atnle  39310  cvratlem  39415  cvrat2  39423  3dim1  39461  2llnjN  39561  2lplnj  39614  linepsubN  39746  pmapsub  39762  paddasslem14  39827  pclfinN  39894  ispsubcl2N  39941  pclfinclN  39944  ldilval  40107  trlord  40563  cdlemk36  40907  dihlsscpre  41228  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  pellexlem5  42821  pellex  42823  pell1234qrmulcl  42843  pellfundex  42874  cantnfresb  43313  omabs2  43321  relexpmulnn  43698  clsk1indlem3  44032  19.41rg  44540  iunconnlem2  44924  relpmin  44942  or2expropbi  47035  fcoresf1  47070  euoreqb  47110  2reu8i  47114  dfatcolem  47256  f1oresf1o2  47292  nltle2tri  47314  imasetpreimafvbijlemf1  47405  iccpartnel  47439  ich2exprop  47472  ichreuopeq  47474  paireqne  47512  prprelprb  47518  reupr  47523  reuopreuprim  47527  fmtnofac2lem  47569  sfprmdvdsmersenne  47604  lighneallem3  47608  lighneallem4  47611  requad2  47624  bgoldbtbnd  47810  dfnbgr6  47857  isubgredg  47866  grimuhgr  47887  grimco  47889  uhgrimedgi  47890  isuspgrimlem  47895  clnbgrgrimlem  47933  grimedg  47935  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedg2ov  48057  gpgedg2iv  48058  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5  48113  pgnbgreunbgrlem6  48114  pgnbgreunbgr  48115  upgrwlkupwlk  48128  ldepspr  48462  affinecomb1  48691  itsclc0  48760  aacllem  49790