Theorem impd 410

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  impcomd  411  imp32  418  imp4b  421  imp4c  423  imp4d  424  imp5d  439  imp5g  441  pm3.31  449  expimpd  453  expl  457  ancomsd  465  syland  603  3expib  1122  ax13lem1  2372  equs5  2458  rsp2  3246  moi  3680  reu6  3688  sbciegftOLD  3782  elpwunsn  4638  opthpr  4805  preqsnd  4813  opthprneg  4819  3elpr2eq  4860  invdisj  5081  snopeqop  5453  solin  5558  sotr2  5565  wefrc  5617  relop  5797  elinxp  5974  reuop  6245  dfpo2  6248  tz7.7  6337  ordtr2  6356  funopsn  7086  tpres  7141  funfvima  7170  isomin  7278  sorpsscmpl  7674  peano5  7833  resf1ext2b  7875  f1oweALT  7914  poxp  8068  soxp  8069  tfr3  8328  tz7.48-1  8372  omordi  8491  odi  8504  omass  8505  oen0  8511  nndi  8548  nnmass  8549  nnmordi  8556  eroveu  8746  ssfi  9097  findcard3  9187  findcard3OLD  9188  fiint  9235  fiintOLD  9236  suplub  9369  hartogs  9455  card2on  9465  unxpwdom2  9499  inf3lem2  9544  ttrclselem2  9641  epfrs  9646  tcel  9660  frr3g  9671  dfac2b  10044  infpssr  10221  isf32lem9  10274  axdc3lem4  10366  axcclem  10370  zorn2lem7  10415  ttukeylem6  10427  brdom6disj  10445  ondomon  10476  inar1  10688  gruen  10725  indpi  10820  nqereu  10842  genpn0  10916  distrlem1pr  10938  distrlem5pr  10940  ltexprlem1  10949  reclem4pr  10963  addsrmo  10986  mulsrmo  10987  supsrlem  11024  lelttr  11224  ltlen  11235  mulgt1OLD  12001  fzind  12592  xrlelttr  13076  xnn0xaddcl  13155  fzen  13462  bernneq  14154  swrdswrdlem  14628  repsdf2  14702  limsupbnd2  15408  mulcn2  15521  prodmolem2  15860  dvdsmod0  16187  lcmfunsnlem1  16566  divgcdcoprm0  16594  maxprmfct  16638  pceu  16776  dvdsprmpweqnn  16815  oddprmdvds  16833  infpnlem1  16840  prmgaplem6  16986  imasaddfnlem  17450  initoeu1  17936  termoeu1  17943  plelttr  18266  gsumval2a  18577  cycsubm  19099  symgfix2  19313  psgnunilem4  19394  lsmmod  19572  efgrelexlemb  19647  imasabl  19773  pgpfac1lem5  19978  rngqiprngimf1lem  21219  rngqiprngimfo  21226  nzerooringczr  21405  lindfrn  21746  mat1dimcrng  22380  dmatelnd  22399  mdetunilem7  22521  cpmatacl  22619  cpmatmcllem  22621  lmss  23201  hausnei2  23256  isnrm2  23261  isnrm3  23262  cmpsublem  23302  2ndcdisj  23359  txcnpi  23511  tx1stc  23553  fgcl  23781  ufileu  23822  fmfnfmlem4  23860  fmfnfm  23861  alexsubALTlem4  23953  alexsubALT  23954  tmdgsum2  23999  prdsxmslem2  24433  ovolicc2  25439  volfiniun  25464  dyadmax  25515  ellimc3  25796  dvlip2  25916  dvne0  25932  dvfsumlem2  25949  taylthlem2  26298  zabsle1  27223  2lgslem3  27331  2sqreulem3  27380  sltlend  27699  scutun12  27739  mulsproplem9  28050  mulsprop  28056  bdayon  28196  eucliddivs  28288  axcontlem4  28930  uhgr2edg  29171  ushgredgedg  29192  ushgredgedgloop  29194  nb3grprlem1  29343  rusgr1vtx  29552  wlkonl1iedg  29627  uhgrwkspthlem2  29717  usgr2wlkneq  29719  usgr2trlncl  29723  uspgrn2crct  29771  wspthsnonn0vne  29880  umgrwwlks2on  29920  elwspths2on  29923  clwlkclwwlkf1lem3  29968  erclwwlktr  29984  erclwwlkntr  30033  frgrnbnb  30255  frgr2wwlk1  30291  frrusgrord  30303  wlkl0  30329  isch3  31203  ocin  31258  shmodsi  31351  spansneleq  31532  stj  32197  atom1d  32315  atcvat2i  32349  chirredlem1  32352  chirredi  32356  mdsymlem3  32367  mdsymlem6  32370  ssdifidlprm  33408  bnj849  34894  pconnconn  35206  cvmsss2  35249  cvmliftlem7  35266  satfv0  35333  satfv0fun  35346  satffunlem  35376  satffunlem1lem1  35377  satffunlem2lem1  35379  mclsind  35545  dfon2lem9  35767  dfon2  35768  cgrextend  35984  btwntriv2  35988  btwncomim  35989  btwnexch3  35996  funtransport  36007  ifscgr  36020  colinearxfr  36051  lineext  36052  fscgr  36056  outsideoftr  36105  trer  36292  finminlem  36294  fnessref  36333  fgmin  36346  bj-andnotim  36564  bj-alanim  36588  bj-0int  37077  relowlssretop  37339  finorwe  37358  finxpsuclem  37373  wl-ax13lem1  37470  poimirlem29  37631  itg2addnclem3  37655  itg2addnc  37656  areacirc  37695  ismtybndlem  37788  heibor1lem  37791  iss2  38314  disjlem17  38779  membpartlem19  38791  prtlem17  38857  riotasvd  38937  lshpsmreu  39090  atnle  39298  cvratlem  39403  cvrat2  39411  3dim1  39449  2llnjN  39549  2lplnj  39602  linepsubN  39734  pmapsub  39750  paddasslem14  39815  pclfinN  39882  ispsubcl2N  39929  pclfinclN  39932  ldilval  40095  trlord  40551  cdlemk36  40895  dihlsscpre  41216  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  pellexlem5  42809  pellex  42811  pell1234qrmulcl  42831  pellfundex  42862  cantnfresb  43300  omabs2  43308  relexpmulnn  43685  clsk1indlem3  44019  19.41rg  44527  iunconnlem2  44911  relpmin  44929  or2expropbi  47022  fcoresf1  47057  euoreqb  47097  2reu8i  47101  dfatcolem  47243  f1oresf1o2  47279  nltle2tri  47301  imasetpreimafvbijlemf1  47392  iccpartnel  47426  ich2exprop  47459  ichreuopeq  47461  paireqne  47499  prprelprb  47505  reupr  47510  reuopreuprim  47514  fmtnofac2lem  47556  sfprmdvdsmersenne  47591  lighneallem3  47595  lighneallem4  47598  requad2  47611  bgoldbtbnd  47797  dfnbgr6  47845  isubgredg  47854  grimuhgr  47875  grimco  47877  uhgrimedgi  47878  isuspgrimlem  47883  clnbgrgrimlem  47921  grimedg  47923  gpgvtxedg0  48051  gpgvtxedg1  48052  gpgedg2ov  48054  gpgedg2iv  48055  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  pgnbgreunbgrlem2lem3  48104  pgnbgreunbgrlem2  48105  pgnbgreunbgrlem3  48106  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5  48111  pgnbgreunbgrlem6  48112  pgnbgreunbgr  48113  upgrwlkupwlk  48128  ldepspr  48462  affinecomb1  48691  itsclc0  48760  aacllem  49790