Theorem impd 413

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  impcomd  414  imp32  421  imp4b  424  imp4c  426  imp4d  427  imp5d  442  imp5g  444  pm3.31  452  expimpd  456  expl  460  ancomsd  468  syland  604  3expib  1118  ax13lem1  2392  equs5  2483  rsp2  3213  moi  3709  reu6  3717  sbciegft  3808  elpwunsn  4621  opthpr  4782  preqsnd  4789  opthprneg  4795  3elpr2eq  4837  invdisj  5050  snopeqop  5396  sotr2  5505  wefrc  5549  relop  5721  elinxp  5890  reuop  6144  tz7.7  6217  ordtr2  6235  funopsn  6910  tpres  6963  funfvima  6992  isomin  7090  sorpsscmpl  7460  peano5  7605  f1oweALT  7673  poxp  7822  soxp  7823  tfr3  8035  tz7.48-1  8079  omordi  8192  odi  8205  omass  8206  oen0  8212  nndi  8249  nnmass  8250  nnmordi  8257  eroveu  8392  findcard3  8761  fiint  8795  suplub  8924  hartogs  9008  card2on  9018  unxpwdom2  9052  inf3lem2  9092  epfrs  9173  tcel  9187  dfac2b  9556  infpssr  9730  isf32lem9  9783  axdc3lem4  9875  axcclem  9879  zorn2lem7  9924  ttukeylem6  9936  brdom6disj  9954  ondomon  9985  inar1  10197  gruen  10234  indpi  10329  nqereu  10351  genpn0  10425  distrlem1pr  10447  distrlem5pr  10449  ltexprlem1  10458  reclem4pr  10472  addsrmo  10495  mulsrmo  10496  supsrlem  10533  lelttr  10731  ltlen  10741  mulgt1  11499  fzind  12081  xrlelttr  12550  xnn0xaddcl  12629  fzen  12925  bernneq  13591  swrdswrdlem  14066  repsdf2  14140  limsupbnd2  14840  mulcn2  14952  prodmolem2  15289  dvdsmod0  15613  lcmfunsnlem1  15981  divgcdcoprm0  16009  maxprmfct  16053  pceu  16183  dvdsprmpweqnn  16221  oddprmdvds  16239  infpnlem1  16246  prmgaplem6  16392  imasaddfnlem  16801  initoeu1  17271  termoeu1  17278  plelttr  17582  gsumval2a  17895  cycsubm  18345  symgfix2  18544  psgnunilem4  18625  lsmmod  18801  efgrelexlemb  18876  pgpfac1lem5  19201  lindfrn  20965  mat1dimcrng  21086  dmatelnd  21105  mdetunilem7  21227  cpmatacl  21324  cpmatmcllem  21326  lmss  21906  hausnei2  21961  isnrm2  21966  isnrm3  21967  cmpsublem  22007  2ndcdisj  22064  txcnpi  22216  tx1stc  22258  fgcl  22486  ufileu  22527  fmfnfmlem4  22565  fmfnfm  22566  alexsubALTlem4  22658  alexsubALT  22659  tmdgsum2  22704  prdsxmslem2  23139  ovolicc2  24123  volfiniun  24148  dyadmax  24199  ellimc3  24477  dvlip2  24592  dvne0  24608  zabsle1  25872  2lgslem3  25980  2sqreulem3  26029  axcontlem4  26753  uhgr2edg  26990  ushgredgedg  27011  ushgredgedgloop  27013  nb3grprlem1  27162  rusgr1vtx  27370  wlkonl1iedg  27447  uhgrwkspthlem2  27535  usgr2wlkneq  27537  usgr2trlncl  27541  uspgrn2crct  27586  wspthsnonn0vne  27696  umgrwwlks2on  27736  elwspths2on  27739  clwlkclwwlkf1lem3  27784  erclwwlktr  27800  erclwwlkntr  27850  frgrnbnb  28072  frgr2wwlk1  28108  frrusgrord  28120  wlkl0  28146  isch3  29018  ocin  29073  shmodsi  29166  spansneleq  29347  stj  30012  atom1d  30130  atcvat2i  30164  chirredlem1  30167  chirredi  30171  mdsymlem3  30182  mdsymlem6  30185  bnj849  32197  pconnconn  32478  cvmsss2  32521  cvmliftlem7  32538  satfv0  32605  satfv0fun  32618  satffunlem  32648  satffunlem1lem1  32649  satffunlem2lem1  32651  mclsind  32817  dfpo2  32991  dfon2lem9  33036  dfon2  33037  frr3g  33121  scutun12  33271  cgrextend  33469  btwntriv2  33473  btwncomim  33474  btwnexch3  33481  funtransport  33492  ifscgr  33505  colinearxfr  33536  lineext  33537  fscgr  33541  outsideoftr  33590  trer  33664  finminlem  33666  fnessref  33705  fgmin  33718  bj-andnotim  33922  bj-alanim  33946  bj-0int  34396  relowlssretop  34647  finorwe  34666  finxpsuclem  34681  wl-ax13lem1  34761  poimirlem29  34936  itg2addnclem3  34960  itg2addnc  34961  areacirc  35002  ismtybndlem  35099  heibor1lem  35102  iss2  35616  prtlem17  36027  riotasvd  36107  lshpsmreu  36260  atnle  36468  cvratlem  36572  cvrat2  36580  3dim1  36618  2llnjN  36718  2lplnj  36771  linepsubN  36903  pmapsub  36919  paddasslem14  36984  pclfinN  37051  ispsubcl2N  37098  pclfinclN  37101  ldilval  37264  trlord  37720  cdlemk36  38064  dihlsscpre  38385  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  pellexlem5  39479  pellex  39481  pell1234qrmulcl  39501  pellfundex  39532  relexpmulnn  40103  clsk1indlem3  40442  19.41rg  40933  iunconnlem2  41318  or2expropbi  43318  euoreqb  43357  2reu8i  43361  dfatcolem  43503  f1oresf1o2  43539  nltle2tri  43562  imasetpreimafvbijlemf1  43613  iccpartnel  43647  ich2exprop  43682  ichreuopeq  43684  paireqne  43722  prprelprb  43728  reupr  43733  reuopreuprim  43737  fmtnofac2lem  43779  sfprmdvdsmersenne  43817  lighneallem3  43821  lighneallem4  43824  requad2  43837  bgoldbtbnd  44023  isomuspgrlem2d  44045  isomgrsym  44050  isomgrtr  44053  upgrwlkupwlk  44064  nzerooringczr  44392  ldepspr  44577  affinecomb1  44738  itsclc0  44807  aacllem  44951