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  2405  equs5  2491  rsp2  3281  moi  3679  reu6  3687  elpwunsn  4648  opthpr  4814  preqsnd  4822  opthprneg  4828  3elpr2eq  4869  invdisj  5093  snopeqop  5487  solin  5594  sotr2  5601  wefrc  5653  relop  5834  elinxp  6016  reuop  6295  dfpo2  6298  tz7.7  6387  ordtr2  6407  funopsnOLD  7149  tpres  7204  funfvima  7233  isomin  7342  sorpsscmpl  7739  peano5  7894  resf1ext2b  7936  f1oweALT  7973  poxp  8130  soxp  8131  tfr3  8392  tz7.48-1  8436  omordi  8557  odi  8570  omass  8571  oen0  8578  nndi  8615  nnmass  8616  nnmordi  8623  eroveu  8816  ssfi  9171  findcard3  9257  fiint  9300  suplub  9434  hartogs  9520  card2on  9530  unxpwdom2  9564  inf3lem2  9612  ttrclselem2  9709  epfrs  9714  tcel  9726  frr3g  9742  dfac2b  10137  infpssr  10314  isf32lem9  10367  axdc3lem4  10459  axcclem  10463  zorn2lem7  10508  ttukeylem6  10520  brdom6disj  10539  ondomon  10575  inar1  10788  gruen  10825  indpi  10920  nqereu  10942  genpn0  11016  distrlem1pr  11038  distrlem5pr  11040  ltexprlem1  11049  reclem4pr  11063  addsrmo  11086  mulsrmo  11087  supsrlem  11124  lelttr  11328  ltlen  11339  fzind  12723  xrlelttr  13211  xnn0xaddcl  13291  fzen  13599  bernneq  14297  swrdswrdlem  14777  repsdf2  14853  limsupbnd2  15574  mulcn2  15687  prodmolem2  16028  dvdsmod0  16354  lcmfunsnlem1  16733  divgcdcoprm0  16761  maxprmfct  16806  pceu  16944  dvdsprmpweqnn  16983  oddprmdvds  17001  infpnlem1  17008  prmgaplem6  17154  imasaddfnlem  17620  initoeu1  18106  termoeu1  18113  plelttr  18436  gsumval2a  18793  cycsubm  19336  symgfix2  19549  psgnunilem4  19630  lsmmod  19808  efgrelexlemb  19883  imasabl  20009  pgpfac1lem5  20214  rngqiprngimf1lem  21503  rngqiprngimfo  21510  ssdifidlprm  21555  nzerooringczr  21699  lindfrn  22040  mat1dimcrng  22705  dmatelnd  22724  mdetunilem7  22846  cpmatacl  22947  cpmatmcllem  22949  lmss  23529  hausnei2  23584  isnrm2  23589  isnrm3  23590  cmpsublem  23630  2ndcdisj  23688  txcnpi  23840  tx1stc  23882  fgcl  24110  ufileu  24151  fmfnfmlem4  24189  fmfnfm  24190  alexsubALTlem4  24282  alexsubALT  24283  tmdgsum2  24328  prdsxmslem2  24761  ovolicc2  25756  volfiniun  25781  dyadmax  25832  ellimc3  26113  dvlip2  26229  dvne0  26245  dvfsumlem2  26261  taylthlem2  26617  zabsle1  27540  2lgslem3  27648  2sqreulem3  27697  ltlesnd  28019  cutsun12  28063  mulsproplem9  28397  mulsprop  28403  bdayons  28549  n0ssoldg  28626  eucliddivs  28649  bdayfinbndlem1  28740  axcontlem4  29432  uhgr2edg  29676  ushgredgedg  29697  ushgredgedgloop  29699  nb3grprlem1  29848  rusgr1vtx  30056  wlkonl1iedg  30131  uhgrwkspthlem2  30227  usgr2wlkneq  30229  usgr2trlncl  30233  uspgrn2crct  30284  wspthsnonn0vne  30393  usgrwwlks2on  30434  umgrwwlks2on  30435  elwspths2on  30438  elwspths2onw  30439  clwlkclwwlkf1lem3  30484  erclwwlktr  30500  erclwwlkntr  30549  frgrnbnb  30781  frgr2wwlk1  30817  frrusgrord  30829  wlkl0  30855  isch3  31730  ocin  31785  shmodsi  31878  spansneleq  32059  stj  32724  atom1d  32842  atcvat2i  32876  chirredlem1  32879  chirredi  32883  mdsymlem3  32894  mdsymlem6  32897  bnj849  35442  fineqvinfep  35659  pconnconn  35818  cvmsss2  35861  cvmliftlem7  35878  satfv0  35945  satfv0fun  35958  satffunlem  35988  satffunlem1lem1  35989  satffunlem2lem1  35991  mclsind  36157  dfon2lem9  36376  dfon2  36377  cgrextend  36596  btwntriv2  36600  btwncomim  36601  btwnexch3  36608  funtransport  36619  ifscgr  36632  colinearxfr  36663  lineext  36664  fscgr  36668  outsideoftr  36717  nmuladdss  36801  trer  36943  finminlem  36945  fnessref  36984  fgmin  36997  axnulregtco  37107  bj-andnotim  37297  bj-alanim  37336  bj-axreprepsep  37828  bj-0int  37859  relowlssretop  38125  finorwe  38144  finxpsuclem  38159  wl-ax13lem1  38256  poimirlem29  38406  itg2addnclem3  38430  itg2addnc  38431  areacirc  38470  ismtybndlem  38564  heibor1lem  38567  iss2  39100  disjlem17  39658  membpartlem19  39670  prtlem17  39757  riotasvd  39837  lshpsmreu  39990  atnle  40198  cvratlem  40302  cvrat2  40310  3dim1  40348  2llnjN  40448  2lplnj  40501  linepsubN  40633  pmapsub  40649  paddasslem14  40714  pclfinN  40781  ispsubcl2N  40828  pclfinclN  40831  ldilval  40994  trlord  41450  cdlemk36  41794  dihlsscpre  42115  baerlem3lem2  42591  baerlem5alem2  42592  baerlem5blem2  42593  pellexlem5  43682  pellex  43684  pell1234qrmulcl  43704  pellfundex  43735  cantnfresb  44173  omabs2  44181  relexpmulnn  44557  clsk1indlem3  44891  19.41rg  45381  iunconnlem2  45765  relpmin  45783  or2expropbi  47930  fcoresf1  47965  euoreqb  48005  2reu8i  48009  dfatcolem  48151  f1oresf1o2  48187  nltle2tri  48209  imasetpreimafvbijlemf1  48312  iccpartnel  48346  ich2exprop  48379  ichreuopeq  48381  paireqne  48419  prprelprb  48425  reupr  48430  reuopreuprim  48434  nprmmul3  48437  fmtnofac2lem  48479  sfprmdvdsmersenne  48514  lighneallem3  48518  lighneallem4  48521  requad2  48547  bgoldbtbnd  48733  dfnbgr6  48781  isubgredg  48790  grimuhgr  48811  grimco  48813  uhgrimedgi  48814  isuspgrimlem  48819  clnbgrgrimlem  48857  grimedg  48859  gpgvtxedg0  48987  gpgvtxedg1  48988  gpgedg2ov  48990  gpgedg2iv  48991  pgnbgreunbgrlem1  49037  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem2  49041  pgnbgreunbgrlem3  49042  pgnbgreunbgrlem4  49043  pgnbgreunbgrlem5  49047  pgnbgreunbgrlem6  49048  pgnbgreunbgr  49049  upgrwlkupwlk  49064  ldepspr  49411  affinecomb1  49640  itsclc0  49709  aacllem  50780