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  1117  ax13lem1  2386  equs5  2477  rsp2  3211  moi  3707  reu6  3715  sbciegft  3806  elpwunsn  4613  opthpr  4774  preqsnd  4781  opthprneg  4787  3elpr2eq  4829  invdisj  5041  snopeqop  5387  sotr2  5498  wefrc  5542  relop  5714  elinxp  5883  reuop  6137  tz7.7  6210  ordtr2  6228  funopsn  6903  tpres  6956  funfvima  6984  isomin  7082  sorpsscmpl  7452  peano5  7597  f1oweALT  7665  poxp  7814  soxp  7815  tfr3  8027  tz7.48-1  8071  omordi  8184  odi  8197  omass  8198  oen0  8204  nndi  8241  nnmass  8242  nnmordi  8249  eroveu  8384  findcard3  8753  fiint  8787  suplub  8916  hartogs  9000  card2on  9010  unxpwdom2  9044  inf3lem2  9084  epfrs  9165  tcel  9179  dfac2b  9548  infpssr  9722  isf32lem9  9775  axdc3lem4  9867  axcclem  9871  zorn2lem7  9916  ttukeylem6  9928  brdom6disj  9946  ondomon  9977  inar1  10189  gruen  10226  indpi  10321  nqereu  10343  genpn0  10417  distrlem1pr  10439  distrlem5pr  10441  ltexprlem1  10450  reclem4pr  10464  addsrmo  10487  mulsrmo  10488  supsrlem  10525  lelttr  10723  ltlen  10733  mulgt1  11491  fzind  12072  xrlelttr  12541  xnn0xaddcl  12620  fzen  12916  bernneq  13582  swrdswrdlem  14058  repsdf2  14132  limsupbnd2  14832  mulcn2  14944  prodmolem2  15281  dvdsmod0  15605  lcmfunsnlem1  15973  divgcdcoprm0  16001  maxprmfct  16045  pceu  16175  dvdsprmpweqnn  16213  oddprmdvds  16231  infpnlem1  16238  prmgaplem6  16384  imasaddfnlem  16793  initoeu1  17263  termoeu1  17270  plelttr  17574  gsumval2a  17887  cycsubm  18337  symgfix2  18536  psgnunilem4  18617  lsmmod  18793  efgrelexlemb  18868  pgpfac1lem5  19193  lindfrn  20957  mat1dimcrng  21078  dmatelnd  21097  mdetunilem7  21219  cpmatacl  21316  cpmatmcllem  21318  lmss  21898  hausnei2  21953  isnrm2  21958  isnrm3  21959  cmpsublem  21999  2ndcdisj  22056  txcnpi  22208  tx1stc  22250  fgcl  22478  ufileu  22519  fmfnfmlem4  22557  fmfnfm  22558  alexsubALTlem4  22650  alexsubALT  22651  tmdgsum2  22696  prdsxmslem2  23131  ovolicc2  24115  volfiniun  24140  dyadmax  24191  ellimc3  24469  dvlip2  24584  dvne0  24600  zabsle1  25864  2lgslem3  25972  2sqreulem3  26021  axcontlem4  26745  uhgr2edg  26982  ushgredgedg  27003  ushgredgedgloop  27005  nb3grprlem1  27154  rusgr1vtx  27362  wlkonl1iedg  27439  uhgrwkspthlem2  27527  usgr2wlkneq  27529  usgr2trlncl  27533  uspgrn2crct  27578  wspthsnonn0vne  27688  umgrwwlks2on  27728  elwspths2on  27731  clwlkclwwlkf1lem3  27776  erclwwlktr  27792  erclwwlkntr  27842  frgrnbnb  28064  frgr2wwlk1  28100  frrusgrord  28112  wlkl0  28138  isch3  29010  ocin  29065  shmodsi  29158  spansneleq  29339  stj  30004  atom1d  30122  atcvat2i  30156  chirredlem1  30159  chirredi  30163  mdsymlem3  30174  mdsymlem6  30177  bnj849  32190  pconnconn  32471  cvmsss2  32514  cvmliftlem7  32531  satfv0  32598  satfv0fun  32611  satffunlem  32641  satffunlem1lem1  32642  satffunlem2lem1  32644  mclsind  32810  dfpo2  32984  dfon2lem9  33029  dfon2  33030  frr3g  33114  scutun12  33264  cgrextend  33462  btwntriv2  33466  btwncomim  33467  btwnexch3  33474  funtransport  33485  ifscgr  33498  colinearxfr  33529  lineext  33530  fscgr  33534  outsideoftr  33583  trer  33657  finminlem  33659  fnessref  33698  fgmin  33711  bj-andnotim  33915  bj-alanim  33939  bj-0int  34385  relowlssretop  34636  finorwe  34655  finxpsuclem  34670  wl-ax13lem1  34738  poimirlem29  34913  itg2addnclem3  34937  itg2addnc  34938  areacirc  34979  ismtybndlem  35076  heibor1lem  35079  iss2  35593  prtlem17  36004  riotasvd  36084  lshpsmreu  36237  atnle  36445  cvratlem  36549  cvrat2  36557  3dim1  36595  2llnjN  36695  2lplnj  36748  linepsubN  36880  pmapsub  36896  paddasslem14  36961  pclfinN  37028  ispsubcl2N  37075  pclfinclN  37078  ldilval  37241  trlord  37697  cdlemk36  38041  dihlsscpre  38362  baerlem3lem2  38838  baerlem5alem2  38839  baerlem5blem2  38840  pellexlem5  39420  pellex  39422  pell1234qrmulcl  39442  pellfundex  39473  relexpmulnn  40044  clsk1indlem3  40383  19.41rg  40874  iunconnlem2  41259  or2expropbi  43259  euoreqb  43298  2reu8i  43302  dfatcolem  43444  f1oresf1o2  43480  nltle2tri  43503  imasetpreimafvbijlemf1  43554  iccpartnel  43588  ich2exprop  43623  ichreuopeq  43625  paireqne  43663  prprelprb  43669  reupr  43674  reuopreuprim  43678  fmtnofac2lem  43720  sfprmdvdsmersenne  43758  lighneallem3  43762  lighneallem4  43765  requad2  43778  bgoldbtbnd  43964  isomuspgrlem2d  43986  isomgrsym  43991  isomgrtr  43994  upgrwlkupwlk  44005  nzerooringczr  44333  ldepspr  44518  affinecomb1  44679  itsclc0  44748  aacllem  44892