Theorem impd 411

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  impcomd  412  imp32  419  imp4b  422  imp4c  424  imp4d  425  imp5d  440  imp5g  442  pm3.31  450  expimpd  454  expl  458  ancomsd  466  syland  602  3expib  1115  ax13lem1  2346  equs5  2440  rsp2  3180  moi  3645  reu6  3651  sbciegft  3737  elpwunsn  4528  opthpr  4689  preqsnd  4696  opthprneg  4702  3elpr2eq  4744  invdisj  4948  snopeqop  5287  sotr2  5393  wefrc  5437  relop  5607  elinxp  5771  reuop  6019  tz7.7  6092  ordtr2  6110  funopsn  6773  tpres  6830  funfvima  6858  isomin  6953  sorpsscmpl  7318  peano5  7461  f1oweALT  7529  poxp  7675  soxp  7676  tfr3  7887  tz7.48-1  7930  omordi  8042  odi  8055  omass  8056  oen0  8062  nndi  8099  nnmass  8100  nnmordi  8107  eroveu  8242  findcard3  8607  fiint  8641  suplub  8770  hartogs  8854  card2on  8864  unxpwdom2  8898  inf3lem2  8938  epfrs  9019  tcel  9033  dfac2b  9402  infpssr  9576  isf32lem9  9629  axdc3lem4  9721  axcclem  9725  zorn2lem7  9770  ttukeylem6  9782  brdom6disj  9800  ondomon  9831  inar1  10043  gruen  10080  indpi  10175  nqereu  10197  genpn0  10271  distrlem1pr  10293  distrlem5pr  10295  ltexprlem1  10304  reclem4pr  10318  addsrmo  10341  mulsrmo  10342  supsrlem  10379  lelttr  10578  ltlen  10588  mulgt1  11347  fzind  11929  xrlelttr  12399  xnn0xaddcl  12478  fzen  12774  bernneq  13440  swrdswrdlem  13902  repsdf2  13976  limsupbnd2  14674  mulcn2  14786  prodmolem2  15122  dvdsmod0  15446  lcmfunsnlem1  15810  divgcdcoprm0  15838  maxprmfct  15882  pceu  16012  dvdsprmpweqnn  16050  oddprmdvds  16068  infpnlem1  16075  prmgaplem6  16221  imasaddfnlem  16630  initoeu1  17100  termoeu1  17107  plelttr  17411  gsumval2a  17718  symgfix2  18275  psgnunilem4  18356  lsmmod  18528  efgrelexlemb  18603  pgpfac1lem5  18918  lindfrn  20647  mat1dimcrng  20770  dmatelnd  20789  mdetunilem7  20911  cpmatacl  21008  cpmatmcllem  21010  lmss  21590  hausnei2  21645  isnrm2  21650  isnrm3  21651  cmpsublem  21691  2ndcdisj  21748  txcnpi  21900  tx1stc  21942  fgcl  22170  ufileu  22211  fmfnfmlem4  22249  fmfnfm  22250  alexsubALTlem4  22342  alexsubALT  22343  tmdgsum2  22388  prdsxmslem2  22822  ovolicc2  23806  volfiniun  23831  dyadmax  23882  ellimc3  24160  dvlip2  24275  dvne0  24291  zabsle1  25554  2lgslem3  25662  2sqreulem3  25711  axcontlem4  26436  uhgr2edg  26673  ushgredgedg  26694  ushgredgedgloop  26696  nb3grprlem1  26845  rusgr1vtx  27053  wlkonl1iedg  27129  uhgrwkspthlem2  27222  usgr2wlkneq  27224  usgr2trlncl  27228  uspgrn2crct  27273  wspthsnonn0vne  27383  umgrwwlks2on  27423  elwspths2on  27426  clwlkclwwlkf1lem3  27471  erclwwlktr  27487  erclwwlkntr  27537  frgrnbnb  27764  frgr2wwlk1  27800  frrusgrord  27812  wlkl0  27838  isch3  28709  ocin  28764  shmodsi  28857  spansneleq  29038  stj  29703  atom1d  29821  atcvat2i  29855  chirredlem1  29858  chirredi  29862  mdsymlem3  29873  mdsymlem6  29876  bnj849  31813  pconnconn  32086  cvmsss2  32129  cvmliftlem7  32146  satfv0  32213  satfv0fun  32226  satffunlem  32256  satffunlem1lem1  32257  satffunlem2lem1  32259  mclsind  32425  dfpo2  32599  dfon2lem9  32644  dfon2  32645  frr3g  32730  scutun12  32880  cgrextend  33078  btwntriv2  33082  btwncomim  33083  btwnexch3  33090  funtransport  33101  ifscgr  33114  colinearxfr  33145  lineext  33146  fscgr  33150  outsideoftr  33199  trer  33273  finminlem  33275  fnessref  33314  fgmin  33327  bj-andnotim  33528  bj-alanim  33552  bj-0int  33992  relowlssretop  34175  finorwe  34194  finxpsuclem  34209  wl-ax13lem1  34277  poimirlem29  34452  itg2addnclem3  34476  itg2addnc  34477  areacirc  34518  ismtybndlem  34616  heibor1lem  34619  iss2  35133  prtlem17  35543  riotasvd  35623  lshpsmreu  35776  atnle  35984  cvratlem  36088  cvrat2  36096  3dim1  36134  2llnjN  36234  2lplnj  36287  linepsubN  36419  pmapsub  36435  paddasslem14  36500  pclfinN  36567  ispsubcl2N  36614  pclfinclN  36617  ldilval  36780  trlord  37236  cdlemk36  37580  dihlsscpre  37901  baerlem3lem2  38377  baerlem5alem2  38378  baerlem5blem2  38379  pellexlem5  38915  pellex  38917  pell1234qrmulcl  38937  pellfundex  38968  relexpmulnn  39539  clsk1indlem3  39878  19.41rg  40423  iunconnlem2  40808  or2expropbi  42785  euoreqb  42824  2reu8i  42828  dfatcolem  42970  f1oresf1o2  43006  nltle2tri  43029  iccpartnel  43080  ich2exprop  43115  ichreuopeq  43117  paireqne  43155  prprelprb  43161  reupr  43166  reuopreuprim  43170  fmtnofac2lem  43212  sfprmdvdsmersenne  43250  lighneallem3  43254  lighneallem4  43257  requad2  43270  bgoldbtbnd  43456  isomuspgrlem2d  43478  isomgrsym  43483  isomgrtr  43486  upgrwlkupwlk  43497  nzerooringczr  43821  ldepspr  44008  affinecomb1  44170  itsclc0  44239  aacllem  44382