Theorem impd 415

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 90	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 411	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 33	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  impcomd  416  imp32  423  imp4b  426  imp4c  428  imp4d  429  imp5d  444  imp5g  446  pm3.31  454  expimpd  458  expl  462  ancomsd  470  syland  614  3expib  1140  ax13lem1  2406  equs5  2492  rsp2  3282  moi  3682  reu6  3690  elpwunsn  4651  opthpr  4817  preqsnd  4825  opthprneg  4831  3elpr2eq  4872  invdisj  5096  snopeqop  5491  solin  5598  sotr2  5605  wefrc  5657  relop  5838  elinxp  6020  reuop  6296  dfpo2  6299  tz7.7  6388  ordtr2  6408  funopsnOLD  7147  tpres  7201  funfvima  7230  isomin  7337  sorpsscmpl  7733  peano5  7891  resf1ext2b  7933  f1oweALT  7970  poxp  8125  soxp  8126  tfr3  8387  tz7.48-1  8431  omordi  8552  odi  8565  omass  8566  oen0  8573  nndi  8610  nnmass  8611  nnmordi  8618  eroveu  8811  ssfi  9158  findcard3  9244  fiint  9287  suplub  9421  hartogs  9507  card2on  9517  unxpwdom2  9551  inf3lem2  9599  ttrclselem2  9696  epfrs  9701  tcel  9713  frr3g  9729  dfac2b  10115  infpssr  10293  isf32lem9  10346  axdc3lem4  10438  axcclem  10442  zorn2lem7  10487  ttukeylem6  10499  brdom6disj  10517  ondomon  10548  inar1  10761  gruen  10798  indpi  10893  nqereu  10915  genpn0  10989  distrlem1pr  11011  distrlem5pr  11013  ltexprlem1  11022  reclem4pr  11036  addsrmo  11059  mulsrmo  11060  supsrlem  11097  lelttr  11301  ltlen  11312  fzind  12695  xrlelttr  13182  xnn0xaddcl  13262  fzen  13570  bernneq  14267  swrdswrdlem  14743  repsdf2  14817  limsupbnd2  15536  mulcn2  15649  prodmolem2  15991  dvdsmod0  16317  lcmfunsnlem1  16696  divgcdcoprm0  16724  maxprmfct  16769  pceu  16907  dvdsprmpweqnn  16946  oddprmdvds  16964  infpnlem1  16971  prmgaplem6  17117  imasaddfnlem  17583  initoeu1  18069  termoeu1  18076  plelttr  18399  gsumval2a  18744  cycsubm  19274  symgfix2  19487  psgnunilem4  19568  lsmmod  19746  efgrelexlemb  19821  imasabl  19947  pgpfac1lem5  20152  rngqiprngimf1lem  21415  rngqiprngimfo  21422  ssdifidlprm  21467  nzerooringczr  21611  lindfrn  21952  mat1dimcrng  22615  dmatelnd  22634  mdetunilem7  22756  cpmatacl  22854  cpmatmcllem  22856  lmss  23436  hausnei2  23491  isnrm2  23496  isnrm3  23497  cmpsublem  23537  2ndcdisj  23594  txcnpi  23746  tx1stc  23788  fgcl  24016  ufileu  24057  fmfnfmlem4  24095  fmfnfm  24096  alexsubALTlem4  24188  alexsubALT  24189  tmdgsum2  24234  prdsxmslem2  24667  ovolicc2  25662  volfiniun  25687  dyadmax  25738  ellimc3  26019  dvlip2  26135  dvne0  26151  dvfsumlem2  26167  taylthlem2  26515  zabsle1  27438  2lgslem3  27546  2sqreulem3  27595  ltlesnd  27917  cutsun12  27961  mulsproplem9  28295  mulsprop  28301  bdayons  28447  n0ssoldg  28524  eucliddivs  28547  bdayfinbndlem1  28638  axcontlem4  29295  uhgr2edg  29536  ushgredgedg  29557  ushgredgedgloop  29559  nb3grprlem1  29708  rusgr1vtx  29916  wlkonl1iedg  29991  uhgrwkspthlem2  30081  usgr2wlkneq  30083  usgr2trlncl  30087  uspgrn2crct  30135  wspthsnonn0vne  30244  usgrwwlks2on  30285  umgrwwlks2on  30286  elwspths2on  30289  elwspths2onw  30290  clwlkclwwlkf1lem3  30335  erclwwlktr  30351  erclwwlkntr  30400  frgrnbnb  30622  frgr2wwlk1  30658  frrusgrord  30670  wlkl0  30696  isch3  31571  ocin  31626  shmodsi  31719  spansneleq  31900  stj  32565  atom1d  32683  atcvat2i  32717  chirredlem1  32720  chirredi  32724  mdsymlem3  32735  mdsymlem6  32738  bnj849  35291  fineqvinfep  35516  pconnconn  35701  cvmsss2  35744  cvmliftlem7  35761  satfv0  35828  satfv0fun  35841  satffunlem  35871  satffunlem1lem1  35872  satffunlem2lem1  35874  mclsind  36040  dfon2lem9  36259  dfon2  36260  cgrextend  36478  btwntriv2  36482  btwncomim  36483  btwnexch3  36490  funtransport  36501  ifscgr  36514  colinearxfr  36545  lineext  36546  fscgr  36550  outsideoftr  36599  nmuladdss  36668  trer  36805  finminlem  36807  fnessref  36846  fgmin  36859  axnulregtco  36969  bj-andnotim  37159  bj-alanim  37198  bj-axreprepsep  37690  bj-0int  37721  relowlssretop  37987  finorwe  38006  finxpsuclem  38021  wl-ax13lem1  38118  poimirlem29  38278  itg2addnclem3  38302  itg2addnc  38303  areacirc  38342  ismtybndlem  38435  heibor1lem  38438  iss2  38971  disjlem17  39529  membpartlem19  39541  prtlem17  39628  riotasvd  39708  lshpsmreu  39861  atnle  40069  cvratlem  40173  cvrat2  40181  3dim1  40219  2llnjN  40319  2lplnj  40372  linepsubN  40504  pmapsub  40520  paddasslem14  40585  pclfinN  40652  ispsubcl2N  40699  pclfinclN  40702  ldilval  40865  trlord  41321  cdlemk36  41665  dihlsscpre  41986  baerlem3lem2  42462  baerlem5alem2  42463  baerlem5blem2  42464  pellexlem5  43540  pellex  43542  pell1234qrmulcl  43562  pellfundex  43593  cantnfresb  44031  omabs2  44039  relexpmulnn  44415  clsk1indlem3  44749  19.41rg  45239  iunconnlem2  45623  relpmin  45641  or2expropbi  47748  fcoresf1  47783  euoreqb  47823  2reu8i  47827  dfatcolem  47969  f1oresf1o2  48005  nltle2tri  48027  imasetpreimafvbijlemf1  48130  iccpartnel  48164  ich2exprop  48197  ichreuopeq  48199  paireqne  48237  prprelprb  48243  reupr  48248  reuopreuprim  48252  nprmmul3  48255  fmtnofac2lem  48297  sfprmdvdsmersenne  48332  lighneallem3  48336  lighneallem4  48339  requad2  48365  bgoldbtbnd  48551  dfnbgr6  48599  isubgredg  48608  grimuhgr  48629  grimco  48631  uhgrimedgi  48632  isuspgrimlem  48637  clnbgrgrimlem  48675  grimedg  48677  gpgvtxedg0  48805  gpgvtxedg1  48806  gpgedg2ov  48808  gpgedg2iv  48809  pgnbgreunbgrlem1  48855  pgnbgreunbgrlem2lem1  48856  pgnbgreunbgrlem2lem2  48857  pgnbgreunbgrlem2lem3  48858  pgnbgreunbgrlem2  48859  pgnbgreunbgrlem3  48860  pgnbgreunbgrlem4  48861  pgnbgreunbgrlem5  48865  pgnbgreunbgrlem6  48866  pgnbgreunbgr  48867  upgrwlkupwlk  48882  ldepspr  49230  affinecomb1  49459  itsclc0  49528  aacllem  50578