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 206  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  603  3expib  1121  ax13lem1  2375  equs5  2461  rsp2  3139  moi  3654  reu6  3662  sbciegft  3755  ss2abdv  3998  elpwunsn  4620  opthpr  4783  preqsnd  4790  opthprneg  4796  3elpr2eq  4839  invdisj  5059  snopeqop  5421  solin  5529  sotr2  5536  wefrc  5584  relop  5762  elinxp  5932  reuop  6200  dfpo2  6203  tz7.7  6296  ordtr2  6314  funopsn  7029  tpres  7085  funfvima  7115  isomin  7217  sorpsscmpl  7596  peano5  7749  peano5OLD  7750  f1oweALT  7824  poxp  7978  soxp  7979  tfr3  8239  tz7.48-1  8283  omordi  8406  odi  8419  omass  8420  oen0  8426  nndi  8463  nnmass  8464  nnmordi  8471  eroveu  8610  ssfi  8965  findcard3  9066  fiint  9100  suplub  9228  hartogs  9312  card2on  9322  unxpwdom2  9356  inf3lem2  9396  ttrclselem2  9493  epfrs  9498  tcel  9512  frr3g  9523  dfac2b  9895  infpssr  10073  isf32lem9  10126  axdc3lem4  10218  axcclem  10222  zorn2lem7  10267  ttukeylem6  10279  brdom6disj  10297  ondomon  10328  inar1  10540  gruen  10577  indpi  10672  nqereu  10694  genpn0  10768  distrlem1pr  10790  distrlem5pr  10792  ltexprlem1  10801  reclem4pr  10815  addsrmo  10838  mulsrmo  10839  supsrlem  10876  lelttr  11074  ltlen  11085  mulgt1  11843  fzind  12427  xrlelttr  12899  xnn0xaddcl  12978  fzen  13282  bernneq  13953  swrdswrdlem  14426  repsdf2  14500  limsupbnd2  15201  mulcn2  15314  prodmolem2  15654  dvdsmod0  15978  lcmfunsnlem1  16351  divgcdcoprm0  16379  maxprmfct  16423  pceu  16556  dvdsprmpweqnn  16595  oddprmdvds  16613  infpnlem1  16620  prmgaplem6  16766  imasaddfnlem  17248  initoeu1  17735  termoeu1  17742  plelttr  18071  gsumval2a  18378  cycsubm  18830  symgfix2  19033  psgnunilem4  19114  lsmmod  19290  efgrelexlemb  19365  pgpfac1lem5  19691  lindfrn  21037  mat1dimcrng  21635  dmatelnd  21654  mdetunilem7  21776  cpmatacl  21874  cpmatmcllem  21876  lmss  22458  hausnei2  22513  isnrm2  22518  isnrm3  22519  cmpsublem  22559  2ndcdisj  22616  txcnpi  22768  tx1stc  22810  fgcl  23038  ufileu  23079  fmfnfmlem4  23117  fmfnfm  23118  alexsubALTlem4  23210  alexsubALT  23211  tmdgsum2  23256  prdsxmslem2  23694  ovolicc2  24695  volfiniun  24720  dyadmax  24771  ellimc3  25052  dvlip2  25168  dvne0  25184  zabsle1  26453  2lgslem3  26561  2sqreulem3  26610  axcontlem4  27344  uhgr2edg  27584  ushgredgedg  27605  ushgredgedgloop  27607  nb3grprlem1  27756  rusgr1vtx  27964  wlkonl1iedg  28042  uhgrwkspthlem2  28131  usgr2wlkneq  28133  usgr2trlncl  28137  uspgrn2crct  28182  wspthsnonn0vne  28291  umgrwwlks2on  28331  elwspths2on  28334  clwlkclwwlkf1lem3  28379  erclwwlktr  28395  erclwwlkntr  28444  frgrnbnb  28666  frgr2wwlk1  28702  frrusgrord  28714  wlkl0  28740  isch3  29612  ocin  29667  shmodsi  29760  spansneleq  29941  stj  30606  atom1d  30724  atcvat2i  30758  chirredlem1  30761  chirredi  30765  mdsymlem3  30776  mdsymlem6  30779  bnj849  32914  pconnconn  33202  cvmsss2  33245  cvmliftlem7  33262  satfv0  33329  satfv0fun  33342  satffunlem  33372  satffunlem1lem1  33373  satffunlem2lem1  33375  mclsind  33541  dfon2lem9  33776  dfon2  33777  scutun12  34013  cgrextend  34319  btwntriv2  34323  btwncomim  34324  btwnexch3  34331  funtransport  34342  ifscgr  34355  colinearxfr  34386  lineext  34387  fscgr  34391  outsideoftr  34440  trer  34514  finminlem  34516  fnessref  34555  fgmin  34568  bj-andnotim  34779  bj-alanim  34803  bj-0int  35281  relowlssretop  35543  finorwe  35562  finxpsuclem  35577  wl-ax13lem1  35674  poimirlem29  35815  itg2addnclem3  35839  itg2addnc  35840  areacirc  35879  ismtybndlem  35973  heibor1lem  35976  iss2  36486  prtlem17  36897  riotasvd  36977  lshpsmreu  37130  atnle  37338  cvratlem  37442  cvrat2  37450  3dim1  37488  2llnjN  37588  2lplnj  37641  linepsubN  37773  pmapsub  37789  paddasslem14  37854  pclfinN  37921  ispsubcl2N  37968  pclfinclN  37971  ldilval  38134  trlord  38590  cdlemk36  38934  dihlsscpre  39255  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  pellexlem5  40662  pellex  40664  pell1234qrmulcl  40684  pellfundex  40715  relexpmulnn  41324  clsk1indlem3  41660  19.41rg  42177  iunconnlem2  42562  or2expropbi  44539  fcoresf1  44574  euoreqb  44612  2reu8i  44616  dfatcolem  44758  f1oresf1o2  44794  nltle2tri  44816  imasetpreimafvbijlemf1  44867  iccpartnel  44901  ich2exprop  44934  ichreuopeq  44936  paireqne  44974  prprelprb  44980  reupr  44985  reuopreuprim  44989  fmtnofac2lem  45031  sfprmdvdsmersenne  45066  lighneallem3  45070  lighneallem4  45073  requad2  45086  bgoldbtbnd  45272  isomuspgrlem2d  45294  isomgrsym  45299  isomgrtr  45302  upgrwlkupwlk  45313  nzerooringczr  45641  ldepspr  45825  affinecomb1  46059  itsclc0  46128  aacllem  46516