Theorem impd 414

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  impcomd  415  imp32  422  imp4b  425  imp4c  427  imp4d  428  imp5d  443  imp5g  445  pm3.31  453  expimpd  457  expl  461  ancomsd  469  syland  606  3expib  1124  ax13lem1  2373  equs5  2459  rsp2  3134  moi  3631  reu6  3639  sbciegft  3732  ss2abdv  3977  elpwunsn  4599  opthpr  4762  preqsnd  4769  opthprneg  4775  3elpr2eq  4818  invdisj  5037  snopeqop  5389  solin  5493  sotr2  5500  wefrc  5545  relop  5719  elinxp  5889  reuop  6156  tz7.7  6239  ordtr2  6257  funopsn  6963  tpres  7016  funfvima  7046  isomin  7146  sorpsscmpl  7522  peano5  7671  peano5OLD  7672  f1oweALT  7745  poxp  7895  soxp  7896  tfr3  8135  tz7.48-1  8179  omordi  8294  odi  8307  omass  8308  oen0  8314  nndi  8351  nnmass  8352  nnmordi  8359  eroveu  8494  ssfi  8851  findcard3  8914  fiint  8948  suplub  9076  hartogs  9160  card2on  9170  unxpwdom2  9204  inf3lem2  9244  epfrs  9347  tcel  9361  frr3g  9372  dfac2b  9744  infpssr  9922  isf32lem9  9975  axdc3lem4  10067  axcclem  10071  zorn2lem7  10116  ttukeylem6  10128  brdom6disj  10146  ondomon  10177  inar1  10389  gruen  10426  indpi  10521  nqereu  10543  genpn0  10617  distrlem1pr  10639  distrlem5pr  10641  ltexprlem1  10650  reclem4pr  10664  addsrmo  10687  mulsrmo  10688  supsrlem  10725  lelttr  10923  ltlen  10933  mulgt1  11691  fzind  12275  xrlelttr  12746  xnn0xaddcl  12825  fzen  13129  bernneq  13796  swrdswrdlem  14269  repsdf2  14343  limsupbnd2  15044  mulcn2  15157  prodmolem2  15497  dvdsmod0  15821  lcmfunsnlem1  16194  divgcdcoprm0  16222  maxprmfct  16266  pceu  16399  dvdsprmpweqnn  16438  oddprmdvds  16456  infpnlem1  16463  prmgaplem6  16609  imasaddfnlem  17033  initoeu1  17517  termoeu1  17524  plelttr  17850  gsumval2a  18157  cycsubm  18609  symgfix2  18808  psgnunilem4  18889  lsmmod  19065  efgrelexlemb  19140  pgpfac1lem5  19466  lindfrn  20783  mat1dimcrng  21374  dmatelnd  21393  mdetunilem7  21515  cpmatacl  21613  cpmatmcllem  21615  lmss  22195  hausnei2  22250  isnrm2  22255  isnrm3  22256  cmpsublem  22296  2ndcdisj  22353  txcnpi  22505  tx1stc  22547  fgcl  22775  ufileu  22816  fmfnfmlem4  22854  fmfnfm  22855  alexsubALTlem4  22947  alexsubALT  22948  tmdgsum2  22993  prdsxmslem2  23427  ovolicc2  24419  volfiniun  24444  dyadmax  24495  ellimc3  24776  dvlip2  24892  dvne0  24908  zabsle1  26177  2lgslem3  26285  2sqreulem3  26334  axcontlem4  27058  uhgr2edg  27296  ushgredgedg  27317  ushgredgedgloop  27319  nb3grprlem1  27468  rusgr1vtx  27676  wlkonl1iedg  27753  uhgrwkspthlem2  27841  usgr2wlkneq  27843  usgr2trlncl  27847  uspgrn2crct  27892  wspthsnonn0vne  28001  umgrwwlks2on  28041  elwspths2on  28044  clwlkclwwlkf1lem3  28089  erclwwlktr  28105  erclwwlkntr  28154  frgrnbnb  28376  frgr2wwlk1  28412  frrusgrord  28424  wlkl0  28450  isch3  29322  ocin  29377  shmodsi  29470  spansneleq  29651  stj  30316  atom1d  30434  atcvat2i  30468  chirredlem1  30471  chirredi  30475  mdsymlem3  30486  mdsymlem6  30489  bnj849  32618  pconnconn  32906  cvmsss2  32949  cvmliftlem7  32966  satfv0  33033  satfv0fun  33046  satffunlem  33076  satffunlem1lem1  33077  satffunlem2lem1  33079  mclsind  33245  dfpo2  33441  dfon2lem9  33486  dfon2  33487  scutun12  33741  cgrextend  34047  btwntriv2  34051  btwncomim  34052  btwnexch3  34059  funtransport  34070  ifscgr  34083  colinearxfr  34114  lineext  34115  fscgr  34119  outsideoftr  34168  trer  34242  finminlem  34244  fnessref  34283  fgmin  34296  bj-andnotim  34507  bj-alanim  34531  bj-0int  35007  relowlssretop  35271  finorwe  35290  finxpsuclem  35305  wl-ax13lem1  35402  poimirlem29  35543  itg2addnclem3  35567  itg2addnc  35568  areacirc  35607  ismtybndlem  35701  heibor1lem  35704  iss2  36216  prtlem17  36627  riotasvd  36707  lshpsmreu  36860  atnle  37068  cvratlem  37172  cvrat2  37180  3dim1  37218  2llnjN  37318  2lplnj  37371  linepsubN  37503  pmapsub  37519  paddasslem14  37584  pclfinN  37651  ispsubcl2N  37698  pclfinclN  37701  ldilval  37864  trlord  38320  cdlemk36  38664  dihlsscpre  38985  baerlem3lem2  39461  baerlem5alem2  39462  baerlem5blem2  39463  pellexlem5  40358  pellex  40360  pell1234qrmulcl  40380  pellfundex  40411  relexpmulnn  40994  clsk1indlem3  41330  19.41rg  41843  iunconnlem2  42228  or2expropbi  44200  fcoresf1  44235  euoreqb  44273  2reu8i  44277  dfatcolem  44419  f1oresf1o2  44455  nltle2tri  44478  imasetpreimafvbijlemf1  44529  iccpartnel  44563  ich2exprop  44596  ichreuopeq  44598  paireqne  44636  prprelprb  44642  reupr  44647  reuopreuprim  44651  fmtnofac2lem  44693  sfprmdvdsmersenne  44728  lighneallem3  44732  lighneallem4  44735  requad2  44748  bgoldbtbnd  44934  isomuspgrlem2d  44956  isomgrsym  44961  isomgrtr  44964  upgrwlkupwlk  44975  nzerooringczr  45303  ldepspr  45487  affinecomb1  45721  itsclc0  45790  aacllem  46176