Theorem impd 446

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  imp32  448  pm3.31  460  syland  497  imp4b  611  imp4c  615  imp4d  616  imp5d  623  expimpd  627  expl  646  3expib  1260  ax13lem1  2236  equs5  2339  rsp2  2920  moi  3356  reu6  3362  sbciegft  3433  elpwunsn  4171  prel12  4323  opthpr  4324  invdisj  4571  reusv1OLD  4793  ralxfrd  4805  ralxfrd2  4810  sotr2  4988  wefrc  5032  relop  5194  elres  5355  iss  5367  tz7.7  5666  ordtr2  5685  funssres  5844  fv3  6116  funopsn  6319  fmptsnd  6340  tpres  6371  funfvima  6396  isomin  6487  sorpsscmpl  6846  peano5  6981  f1oweALT  7043  poxp  7176  soxp  7177  wfr3g  7300  tfr3  7382  tz7.48-1  7425  omordi  7533  odi  7546  omass  7547  oen0  7553  nndi  7590  nnmass  7591  nnmordi  7598  nnmord  7599  eroveu  7729  findcard3  8088  fiint  8122  suplub  8249  hartogs  8332  card2on  8342  unxpwdom2  8376  inf3lem2  8409  epfrs  8490  tcel  8504  dfac2  8836  cfcoflem  8977  infpssr  9013  isf32lem9  9066  axdc3lem4  9158  axcclem  9162  zorn2lem7  9207  ttukeylem6  9219  brdom6disj  9235  ondomon  9264  inar1  9476  gruen  9513  indpi  9608  nqereu  9630  genpn0  9704  distrlem1pr  9726  distrlem5pr  9728  ltexprlem1  9737  reclem4pr  9751  addsrmo  9773  mulsrmo  9774  supsrlem  9811  lelttr  10007  ltletr  10008  ltlen  10017  mulgt1  10761  fzind  11351  eqreznegel  11650  xrlelttr  11863  xrltletr  11864  xnn0xaddcl  11940  fzen  12229  elfzodifsumelfzo  12401  bernneq  12852  fundmge2nop0  13129  swrdswrdlem  13311  wrd2ind  13329  reuccats1lem  13331  swrdccatin1  13334  repsdf2  13376  limsupbnd2  14062  rlimuni  14129  mulcn2  14174  rlimno1  14232  prodmolem2  14504  ndvdssub  14971  lcmfunsnlem1  15188  lcmfunsnlem2  15191  coprmdvds  15204  coprmdvdsOLD  15205  coprmdvds2  15206  divgcdcoprm0  15217  maxprmfct  15259  pceu  15389  dvdsprmpweqnn  15427  oddprmdvds  15445  infpnlem1  15452  prmgaplem6  15598  imasaddfnlem  16011  initoeu1  16484  termoeu1  16491  plelttr  16795  gsumval2a  17102  symgfix2  17659  gsmsymgrfixlem1  17670  psgnunilem4  17740  lsmmod  17911  lsmdisj2  17918  efgrelexlemb  17986  pgpfac1lem5  18301  lindfrn  19979  mat1dimcrng  20102  dmatelnd  20121  mdetunilem7  20243  cpmatacl  20340  cpmatmcllem  20342  chfacfisf  20478  chfacfisfcpmat  20479  lmss  20912  lmcnp  20918  hausnei2  20967  isnrm2  20972  isnrm3  20973  cmpsublem  21012  2ndcdisj  21069  1stccnp  21075  txcnpi  21221  txlm  21261  tx1stc  21263  fgss2  21488  fgfil  21489  fgcl  21492  ufileu  21533  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  fmfnfm  21572  ufilcmp  21646  cnpfcf  21655  alexsubALTlem2  21662  alexsubALTlem4  21664  alexsubALT  21665  tmdgsum2  21710  tsmsxp  21768  prdsxmslem2  22144  ivthlem2  23028  ivthlem3  23029  ovolicc2  23097  volfiniun  23122  dyadmax  23172  ellimc3  23449  dvlip2  23562  dvne0  23578  zabsle1  24821  2lgslem3  24929  axcontlem4  25647  umgrislfupgrlem  25788  usgra2edg  25911  usgrares1  25939  nb3graprlem1  25980  iswlkg  26052  usgrcyclnl1  26168  nvnencycllem  26171  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  wwlknred  26251  erclwwlktr  26343  erclwwlkntr  26355  clwlkfoclwwlk  26372  el2wlkonotot0  26399  frg2woteq  26587  numclwwlkovf2ex  26613  frgraregord013  26645  isch3  27482  ocin  27539  shmodsi  27632  spansneleq  27813  stj  28478  atom1d  28596  atcvat2i  28630  chirredlem1  28633  chirredi  28637  mdsymlem3  28648  mdsymlem6  28651  bnj849  30249  pconcon  30467  cvmsss2  30510  cvmliftlem7  30527  mclsind  30721  dfpo2  30898  dfon2lem9  30940  dfon2  30941  frr3g  31023  frrlem11  31036  cgrextend  31285  btwntriv2  31289  btwncomim  31290  btwnexch3  31297  funtransport  31308  ifscgr  31321  colinearxfr  31352  lineext  31353  fscgr  31357  outsideoftr  31406  trer  31480  finminlem  31482  fnessref  31522  fgmin  31535  bj-andnotim  31746  bj-alanim  31781  relowlssretop  32387  finxpsuclem  32410  wl-ax13lem1  32466  poimirlem29  32608  itg2addnclem3  32633  itg2addnc  32634  areacirc  32675  ismtybndlem  32775  heibor1lem  32778  prtlem17  33179  riotasvd  33260  lshpsmreu  33414  atnle  33622  cvratlem  33725  cvrat2  33733  3dim1  33771  2llnjN  33871  2lplnj  33924  linepsubN  34056  pmapsub  34072  paddasslem14  34137  pclfinN  34204  ispsubcl2N  34251  pclfinclN  34254  ldilval  34417  trlord  34875  cdlemk36  35219  dihlsscpre  35541  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  pellexlem5  36415  pellex  36417  pell1234qrmulcl  36437  pellfundex  36468  relexpmulnn  37020  clsk1indlem3  37361  19.41rg  37787  iunconlem2  38193  nltle2tri  39942  iccpartnel  39976  fmtnofac2lem  40018  sfprmdvdsmersenne  40058  lighneallem3  40062  lighneallem4  40065  bgoldbtbnd  40225  uhgr2edg  40435  ushgredgedga  40456  ushgredgedgaloop  40458  nb3grprlem1  40608  rusgr1vtx  40788  upgr1wlkwlk  40847  1wlkv0  40859  wlkOnl1iedg  40873  sPthdifv  40939  uhgr1wlkspthlem2  40960  usgr2wlkneq  40962  usgr2trlncl  40966  usgr2pth  40970  cyclnsPth  41006  uspgrn2crct  41011  wspthsnonn0vne  41124  wwlks2onv  41158  umgrwwlks2on  41161  elwspths2on  41163  erclwwlkstr  41243  erclwwlksntr  41255  frgrnbnb  41463  av-numclwwlkovf2ex  41517  av-frgraregord013  41549  nzerooringczr  41864  ldepspr  42056  aacllem  42356