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  2403  equs5  2489  rsp2  3279  moi  3675  reu6  3683  elpwunsn  4641  opthpr  4805  preqsnd  4813  opthprneg  4819  3elpr2eq  4833  invdisj  5088  snopeqop  5477  solin  5585  sotr2  5592  wefrc  5644  relop  5827  elinxp  6007  reuop  6296  dfpo2  6299  tz7.7  6388  ordtr2  6408  funopsnOLD  7152  tpres  7207  funfvima  7236  isomin  7345  sorpsscmpl  7750  peano5  7905  resf1ext2b  7947  f1oweALT  7984  poxp  8142  soxp  8143  tfr3  8410  tz7.48-1  8456  omordi  8577  odi  8590  omass  8591  oen0  8598  nndi  8635  nnmass  8636  nnmordi  8643  eroveu  8836  ssfi  9191  findcard3  9277  fiint  9321  suplub  9455  hartogs  9541  card2on  9551  unxpwdom2  9585  inf3lem2  9633  ttrclselem2  9730  epfrs  9735  tcel  9747  frr3g  9763  dfac2b  10212  infpssr  10389  isf32lem9  10442  axdc3lem4  10534  axcclem  10538  zorn2lem7  10583  ttukeylem6  10595  brdom6disj  10614  ondomon  10650  inar1  10863  gruen  10900  indpi  10995  nqereu  11017  genpn0  11091  distrlem1pr  11113  distrlem5pr  11115  ltexprlem1  11124  reclem4pr  11138  addsrmo  11161  mulsrmo  11162  supsrlem  11199  lelttr  11403  ltlen  11414  fzind  12800  xrlelttr  13288  xnn0xaddcl  13368  fzen  13677  bernneq  14376  swrdswrdlem  14857  repsdf2  14933  limsupbnd2  15655  mulcn2  15768  prodmolem2  16107  dvdsmod0  16433  lcmfunsnlem1  16817  divgcdcoprm0  16845  maxprmfct  16890  pceu  17029  dvdsprmpweqnn  17068  oddprmdvds  17086  infpnlem1  17093  prmgaplem6  17239  imasaddfnlem  17705  initoeu1  18191  termoeu1  18198  plelttr  18521  gsumval2a  18879  cycsubm  19422  symgfix2  19635  psgnunilem4  19716  lsmmod  19894  efgrelexlemb  19969  imasabl  20095  pgpfac1lem5  20300  rngqiprngimf1lem  21595  rngqiprngimfo  21602  ssdifidlprm  21647  nzerooringczr  21791  lindfrn  22132  mat1dimcrng  22797  dmatelnd  22816  mdetunilem7  22938  cpmatacl  23039  cpmatmcllem  23041  lmss  23621  hausnei2  23676  isnrm2  23681  isnrm3  23682  cmpsublem  23722  2ndcdisj  23780  txcnpi  23932  tx1stc  23974  fgcl  24202  ufileu  24243  fmfnfmlem4  24281  fmfnfm  24282  alexsubALTlem4  24374  alexsubALT  24375  tmdgsum2  24420  prdsxmslem2  24853  ovolicc2  25848  volfiniun  25873  dyadmax  25924  ellimc3  26204  dvlip2  26320  dvne0  26336  dvfsumlem2  26352  taylthlem2  26706  zabsle1  27628  2lgslem3  27736  2sqreulem3  27785  ltlesnd  28137  cutsun12  28181  mulsproplem9  28515  mulsprop  28521  bdayons  28667  n0ssoldg  28744  eucliddivs  28767  bdayfinbndlem1  28858  axcontlem4  29550  uhgr2edg  29794  ushgredgedg  29815  ushgredgedgloop  29817  nb3grprlem1  29966  rusgr1vtx  30174  wlkonl1iedg  30249  uhgrwkspthlem2  30345  usgr2wlkneq  30347  usgr2trlncl  30351  uspgrn2crct  30402  wspthsnonn0vne  30511  usgrwwlks2on  30552  umgrwwlks2on  30553  elwspths2on  30556  elwspths2onw  30557  clwlkclwwlkf1lem3  30602  erclwwlktr  30618  erclwwlkntr  30667  frgrnbnb  30899  frgr2wwlk1  30935  frrusgrord  30947  wlkl0  30973  isch3  31848  ocin  31903  shmodsi  31996  spansneleq  32177  stj  32842  atom1d  32960  atcvat2i  32994  chirredlem1  32997  chirredi  33001  mdsymlem3  33012  mdsymlem6  33015  bnj849  35601  reu6f  35755  soinfdom  35768  fineqvinfep  35849  pconnconn  36082  cvmsss2  36125  cvmliftlem7  36142  satfv0  36209  satfv0fun  36222  satffunlem  36252  satffunlem1lem1  36253  satffunlem2lem1  36255  mclsind  36421  dfon2lem9  36645  dfon2  36646  cgrextend  36865  btwntriv2  36869  btwncomim  36870  btwnexch3  36877  funtransport  36888  ifscgr  36901  colinearxfr  36932  lineext  36933  fscgr  36937  outsideoftr  36986  nmuladdss  37054  trer  37196  finminlem  37198  fnessref  37237  fgmin  37250  axnulregtco  37360  bj-andnotim  37550  bj-alanim  37589  bj-axreprepsep  38083  bj-0int  38114  relowlssretop  38379  finorwe  38398  finxpsuclem  38413  wl-ax13lem1  38510  poimirlem29  38660  itg2addnclem3  38684  itg2addnc  38685  areacirc  38724  ismtybndlem  38833  heibor1lem  38836  iss2  39369  disjlem17  39927  membpartlem19  39939  prtlem17  40026  riotasvd  40106  lshpsmreu  40259  atnle  40467  cvratlem  40571  cvrat2  40579  3dim1  40617  2llnjN  40717  2lplnj  40770  linepsubN  40902  pmapsub  40918  paddasslem14  40983  pclfinN  41050  ispsubcl2N  41097  pclfinclN  41100  ldilval  41263  trlord  41719  cdlemk36  42063  dihlsscpre  42384  baerlem3lem2  42860  baerlem5alem2  42861  baerlem5blem2  42862  pellexlem5  43933  pellex  43935  pell1234qrmulcl  43955  pellfundex  43986  cantnfresb  44419  omabs2  44427  relexpmulnn  44802  clsk1indlem3  45136  19.41rg  45626  iunconnlem2  46010  cocanss2  46015  relpmin  46035  or2expropbi  48197  fcoresf1  48232  euoreqb  48272  2reu8i  48276  dfatcolem  48418  f1oresf1o2  48454  nltle2tri  48476  imasetpreimafvbijlemf1  48579  iccpartnel  48613  ich2exprop  48646  ichreuopeq  48648  paireqne  48686  prprelprb  48692  reupr  48697  reuopreuprim  48701  nprmmul3  48704  fmtnofac2lem  48746  sfprmdvdsmersenne  48781  lighneallem3  48785  lighneallem4  48788  requad2  48814  bgoldbtbnd  49000  dfnbgr6  49048  isubgredg  49057  grimuhgr  49078  grimco  49080  uhgrimedgi  49081  isuspgrimlem  49086  clnbgrgrimlem  49124  grimedg  49126  gpgvtxedg0  49254  gpgvtxedg1  49255  gpgedg2ov  49257  gpgedg2iv  49258  pgnbgreunbgrlem1  49304  pgnbgreunbgrlem2lem1  49305  pgnbgreunbgrlem2lem2  49306  pgnbgreunbgrlem2lem3  49307  pgnbgreunbgrlem2  49308  pgnbgreunbgrlem3  49309  pgnbgreunbgrlem4  49310  pgnbgreunbgrlem5  49314  pgnbgreunbgrlem6  49315  pgnbgreunbgr  49316  upgrwlkupwlk  49331  ldepspr  49678  affinecomb1  49907  itsclc0  49976  aacllem  51107