Theorem impd 411

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  impcomd  412  imp32  419  imp4b  422  imp4c  424  imp4d  425  imp5d  440  imp5g  442  pm3.31  450  expimpd  454  expl  458  ancomsd  466  syland  609  3expib  1128  ax13lem1  2382  equs5  2468  rsp2  3257  moi  3666  reu6  3674  elpwunsn  4623  opthpr  4789  preqsnd  4797  opthprneg  4803  3elpr2eq  4844  invdisj  5065  snopeqop  5454  solin  5560  sotr2  5567  wefrc  5619  relop  5799  elinxp  5978  reuop  6251  dfpo2  6254  tz7.7  6343  ordtr2  6362  funopsnOLD  7098  tpres  7152  funfvima  7181  isomin  7288  sorpsscmpl  7684  peano5  7840  resf1ext2b  7882  f1oweALT  7921  poxp  8075  soxp  8076  tfr3  8335  tz7.48-1  8379  omordi  8498  odi  8511  omass  8512  oen0  8519  nndi  8556  nnmass  8557  nnmordi  8564  eroveu  8756  ssfi  9104  findcard3  9190  fiint  9234  suplub  9370  hartogs  9456  card2on  9466  unxpwdom2  9500  inf3lem2  9548  ttrclselem2  9645  epfrs  9650  tcel  9662  frr3g  9678  dfac2b  10051  infpssr  10228  isf32lem9  10281  axdc3lem4  10373  axcclem  10377  zorn2lem7  10422  ttukeylem6  10434  brdom6disj  10452  ondomon  10483  inar1  10696  gruen  10733  indpi  10828  nqereu  10850  genpn0  10924  distrlem1pr  10946  distrlem5pr  10948  ltexprlem1  10957  reclem4pr  10971  addsrmo  10994  mulsrmo  10995  supsrlem  11032  lelttr  11234  ltlen  11245  mulgt1OLD  12012  fzind  12625  xrlelttr  13105  xnn0xaddcl  13185  fzen  13493  bernneq  14189  swrdswrdlem  14664  repsdf2  14738  limsupbnd2  15443  mulcn2  15556  prodmolem2  15898  dvdsmod0  16225  lcmfunsnlem1  16604  divgcdcoprm0  16632  maxprmfct  16677  pceu  16815  dvdsprmpweqnn  16854  oddprmdvds  16872  infpnlem1  16879  prmgaplem6  17025  imasaddfnlem  17490  initoeu1  17976  termoeu1  17983  plelttr  18306  gsumval2a  18651  cycsubm  19175  symgfix2  19389  psgnunilem4  19470  lsmmod  19648  efgrelexlemb  19723  imasabl  19849  pgpfac1lem5  20054  rngqiprngimf1lem  21294  rngqiprngimfo  21301  nzerooringczr  21462  lindfrn  21803  mat1dimcrng  22467  dmatelnd  22486  mdetunilem7  22608  cpmatacl  22706  cpmatmcllem  22708  lmss  23288  hausnei2  23343  isnrm2  23348  isnrm3  23349  cmpsublem  23389  2ndcdisj  23446  txcnpi  23598  tx1stc  23640  fgcl  23868  ufileu  23909  fmfnfmlem4  23947  fmfnfm  23948  alexsubALTlem4  24040  alexsubALT  24041  tmdgsum2  24086  prdsxmslem2  24519  ovolicc2  25514  volfiniun  25539  dyadmax  25590  ellimc3  25871  dvlip2  25987  dvne0  26003  dvfsumlem2  26019  taylthlem2  26364  zabsle1  27284  2lgslem3  27392  2sqreulem3  27441  ltlesnd  27764  cutsun12  27807  mulsproplem9  28141  mulsprop  28147  bdayons  28293  n0ssoldg  28370  eucliddivs  28393  bdayfinbndlem1  28484  axcontlem4  29061  uhgr2edg  29302  ushgredgedg  29323  ushgredgedgloop  29325  nb3grprlem1  29474  rusgr1vtx  29682  wlkonl1iedg  29757  uhgrwkspthlem2  29847  usgr2wlkneq  29849  usgr2trlncl  29853  uspgrn2crct  29901  wspthsnonn0vne  30010  usgrwwlks2on  30051  umgrwwlks2on  30052  elwspths2on  30055  elwspths2onw  30056  clwlkclwwlkf1lem3  30101  erclwwlktr  30117  erclwwlkntr  30166  frgrnbnb  30388  frgr2wwlk1  30424  frrusgrord  30436  wlkl0  30462  isch3  31337  ocin  31392  shmodsi  31485  spansneleq  31666  stj  32331  atom1d  32449  atcvat2i  32483  chirredlem1  32486  chirredi  32490  mdsymlem3  32501  mdsymlem6  32504  ssdifidlprm  33548  bnj849  35114  fineqvinfep  35313  pconnconn  35466  cvmsss2  35509  cvmliftlem7  35526  satfv0  35593  satfv0fun  35606  satffunlem  35636  satffunlem1lem1  35637  satffunlem2lem1  35639  mclsind  35805  dfon2lem9  36024  dfon2  36025  cgrextend  36243  btwntriv2  36247  btwncomim  36248  btwnexch3  36255  funtransport  36266  ifscgr  36279  colinearxfr  36310  lineext  36311  fscgr  36315  outsideoftr  36364  trer  36551  finminlem  36553  fnessref  36592  fgmin  36605  axnulregtco  36715  bj-andnotim  36906  bj-alanim  36945  bj-axreprepsep  37435  bj-0int  37466  relowlssretop  37732  finorwe  37751  finxpsuclem  37766  wl-ax13lem1  37863  poimirlem29  38023  itg2addnclem3  38047  itg2addnc  38048  areacirc  38087  ismtybndlem  38180  heibor1lem  38183  iss2  38718  disjlem17  39276  membpartlem19  39288  prtlem17  39375  riotasvd  39455  lshpsmreu  39608  atnle  39816  cvratlem  39920  cvrat2  39928  3dim1  39966  2llnjN  40066  2lplnj  40119  linepsubN  40251  pmapsub  40267  paddasslem14  40332  pclfinN  40399  ispsubcl2N  40446  pclfinclN  40449  ldilval  40612  trlord  41068  cdlemk36  41412  dihlsscpre  41733  baerlem3lem2  42209  baerlem5alem2  42210  baerlem5blem2  42211  pellexlem5  43285  pellex  43287  pell1234qrmulcl  43307  pellfundex  43338  cantnfresb  43776  omabs2  43784  relexpmulnn  44160  clsk1indlem3  44494  19.41rg  45001  iunconnlem2  45385  relpmin  45403  or2expropbi  47504  fcoresf1  47539  euoreqb  47579  2reu8i  47583  dfatcolem  47725  f1oresf1o2  47761  nltle2tri  47783  imasetpreimafvbijlemf1  47886  iccpartnel  47920  ich2exprop  47953  ichreuopeq  47955  paireqne  47993  prprelprb  47999  reupr  48004  reuopreuprim  48008  nprmmul3  48011  fmtnofac2lem  48053  sfprmdvdsmersenne  48088  lighneallem3  48092  lighneallem4  48095  requad2  48121  bgoldbtbnd  48307  dfnbgr6  48355  isubgredg  48364  grimuhgr  48385  grimco  48387  uhgrimedgi  48388  isuspgrimlem  48393  clnbgrgrimlem  48431  grimedg  48433  gpgvtxedg0  48561  gpgvtxedg1  48562  gpgedg2ov  48564  gpgedg2iv  48565  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem2lem1  48612  pgnbgreunbgrlem2lem2  48613  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem2  48615  pgnbgreunbgrlem3  48616  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5  48621  pgnbgreunbgrlem6  48622  pgnbgreunbgr  48623  upgrwlkupwlk  48638  ldepspr  48971  affinecomb1  49200  itsclc0  49269  aacllem  50298