Theorem impd 416

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  impcomd  417  imp32  424  imp4b  427  imp4c  429  imp4d  430  imp5d  445  imp5g  447  pm3.31  455  expimpd  459  expl  463  ancomsd  471  syland  615  3expib  1140  ax13lem1  2409  equs5  2495  rsp2  3285  moi  3684  reu6  3692  elpwunsn  4655  opthpr  4821  preqsnd  4829  opthprneg  4835  3elpr2eq  4876  invdisj  5100  snopeqop  5494  solin  5601  sotr2  5608  wefrc  5660  relop  5841  elinxp  6023  reuop  6301  dfpo2  6304  tz7.7  6393  ordtr2  6413  funopsnOLD  7152  tpres  7206  funfvima  7235  isomin  7346  sorpsscmpl  7744  peano5  7899  resf1ext2b  7941  f1oweALT  7978  poxp  8133  soxp  8134  tfr3  8395  tz7.48-1  8439  omordi  8560  odi  8573  omass  8574  oen0  8581  nndi  8618  nnmass  8619  nnmordi  8626  eroveu  8819  ssfi  9167  findcard3  9253  fiint  9296  suplub  9430  hartogs  9516  card2on  9526  unxpwdom2  9560  inf3lem2  9608  ttrclselem2  9705  epfrs  9710  tcel  9722  frr3g  9738  dfac2b  10133  infpssr  10310  isf32lem9  10363  axdc3lem4  10455  axcclem  10459  zorn2lem7  10504  ttukeylem6  10516  brdom6disj  10534  ondomon  10565  inar1  10778  gruen  10815  indpi  10910  nqereu  10932  genpn0  11006  distrlem1pr  11028  distrlem5pr  11030  ltexprlem1  11039  reclem4pr  11053  addsrmo  11076  mulsrmo  11077  supsrlem  11114  lelttr  11318  ltlen  11329  fzind  12712  xrlelttr  13199  xnn0xaddcl  13279  fzen  13587  bernneq  14285  swrdswrdlem  14765  repsdf2  14841  limsupbnd2  15560  mulcn2  15673  prodmolem2  16015  dvdsmod0  16341  lcmfunsnlem1  16720  divgcdcoprm0  16748  maxprmfct  16793  pceu  16931  dvdsprmpweqnn  16970  oddprmdvds  16988  infpnlem1  16995  prmgaplem6  17141  imasaddfnlem  17607  initoeu1  18093  termoeu1  18100  plelttr  18423  gsumval2a  18772  cycsubm  19304  symgfix2  19517  psgnunilem4  19598  lsmmod  19776  efgrelexlemb  19851  imasabl  19977  pgpfac1lem5  20182  rngqiprngimf1lem  21471  rngqiprngimfo  21478  ssdifidlprm  21523  nzerooringczr  21667  lindfrn  22008  mat1dimcrng  22671  dmatelnd  22690  mdetunilem7  22812  cpmatacl  22910  cpmatmcllem  22912  lmss  23492  hausnei2  23547  isnrm2  23552  isnrm3  23553  cmpsublem  23593  2ndcdisj  23650  txcnpi  23802  tx1stc  23844  fgcl  24072  ufileu  24113  fmfnfmlem4  24151  fmfnfm  24152  alexsubALTlem4  24244  alexsubALT  24245  tmdgsum2  24290  prdsxmslem2  24723  ovolicc2  25718  volfiniun  25743  dyadmax  25794  ellimc3  26075  dvlip2  26191  dvne0  26207  dvfsumlem2  26223  taylthlem2  26574  zabsle1  27497  2lgslem3  27605  2sqreulem3  27654  ltlesnd  27976  cutsun12  28020  mulsproplem9  28354  mulsprop  28360  bdayons  28506  n0ssoldg  28583  eucliddivs  28606  bdayfinbndlem1  28697  axcontlem4  29354  uhgr2edg  29595  ushgredgedg  29616  ushgredgedgloop  29618  nb3grprlem1  29767  rusgr1vtx  29975  wlkonl1iedg  30050  uhgrwkspthlem2  30140  usgr2wlkneq  30142  usgr2trlncl  30146  uspgrn2crct  30194  wspthsnonn0vne  30303  usgrwwlks2on  30344  umgrwwlks2on  30345  elwspths2on  30348  elwspths2onw  30349  clwlkclwwlkf1lem3  30394  erclwwlktr  30410  erclwwlkntr  30459  frgrnbnb  30681  frgr2wwlk1  30717  frrusgrord  30729  wlkl0  30755  isch3  31630  ocin  31685  shmodsi  31778  spansneleq  31959  stj  32624  atom1d  32742  atcvat2i  32776  chirredlem1  32779  chirredi  32783  mdsymlem3  32794  mdsymlem6  32797  bnj849  35344  fineqvinfep  35561  pconnconn  35743  cvmsss2  35786  cvmliftlem7  35803  satfv0  35870  satfv0fun  35883  satffunlem  35913  satffunlem1lem1  35914  satffunlem2lem1  35916  mclsind  36082  dfon2lem9  36301  dfon2  36302  cgrextend  36520  btwntriv2  36524  btwncomim  36525  btwnexch3  36532  funtransport  36543  ifscgr  36556  colinearxfr  36587  lineext  36588  fscgr  36592  outsideoftr  36641  nmuladdss  36725  trer  36867  finminlem  36869  fnessref  36908  fgmin  36921  axnulregtco  37031  bj-andnotim  37221  bj-alanim  37260  bj-axreprepsep  37752  bj-0int  37783  relowlssretop  38049  finorwe  38068  finxpsuclem  38083  wl-ax13lem1  38180  poimirlem29  38340  itg2addnclem3  38364  itg2addnc  38365  areacirc  38404  ismtybndlem  38497  heibor1lem  38500  iss2  39033  disjlem17  39591  membpartlem19  39603  prtlem17  39690  riotasvd  39770  lshpsmreu  39923  atnle  40131  cvratlem  40235  cvrat2  40243  3dim1  40281  2llnjN  40381  2lplnj  40434  linepsubN  40566  pmapsub  40582  paddasslem14  40647  pclfinN  40714  ispsubcl2N  40761  pclfinclN  40764  ldilval  40927  trlord  41383  cdlemk36  41727  dihlsscpre  42048  baerlem3lem2  42524  baerlem5alem2  42525  baerlem5blem2  42526  pellexlem5  43600  pellex  43602  pell1234qrmulcl  43622  pellfundex  43653  cantnfresb  44091  omabs2  44099  relexpmulnn  44475  clsk1indlem3  44809  19.41rg  45299  iunconnlem2  45683  relpmin  45701  or2expropbi  47811  fcoresf1  47846  euoreqb  47886  2reu8i  47890  dfatcolem  48032  f1oresf1o2  48068  nltle2tri  48090  imasetpreimafvbijlemf1  48193  iccpartnel  48227  ich2exprop  48260  ichreuopeq  48262  paireqne  48300  prprelprb  48306  reupr  48311  reuopreuprim  48315  nprmmul3  48318  fmtnofac2lem  48360  sfprmdvdsmersenne  48395  lighneallem3  48399  lighneallem4  48402  requad2  48428  bgoldbtbnd  48614  dfnbgr6  48662  isubgredg  48671  grimuhgr  48692  grimco  48694  uhgrimedgi  48695  isuspgrimlem  48700  clnbgrgrimlem  48738  grimedg  48740  gpgvtxedg0  48868  gpgvtxedg1  48869  gpgedg2ov  48871  gpgedg2iv  48872  pgnbgreunbgrlem1  48918  pgnbgreunbgrlem2lem1  48919  pgnbgreunbgrlem2lem2  48920  pgnbgreunbgrlem2lem3  48921  pgnbgreunbgrlem2  48922  pgnbgreunbgrlem3  48923  pgnbgreunbgrlem4  48924  pgnbgreunbgrlem5  48928  pgnbgreunbgrlem6  48929  pgnbgreunbgr  48930  upgrwlkupwlk  48945  ldepspr  49293  affinecomb1  49522  itsclc0  49591  aacllem  50661