Theorem impancom 457

Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)

Hypothesis

Ref	Expression
impancom.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
impancom	⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Proof of Theorem impancom

Step	Hyp	Ref	Expression
1		impancom.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 418	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 87	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 412	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:  mo4  2591  spc2ed  3555  rexraleqim  3601  prsrcmpltd  4433  disjiun  5091  disjord  5092  disjiund  5094  propeqop  5484  euotd  5490  pwssun  5547  iotan0  6523  funopsn  7144  funopsnOLD  7145  isotr  7337  funeldmb  7362  resf1extb  7931  funfv1st2nd  8043  funelss  8044  el2mpocsbcl  8082  ressuppssdif  8183  oeordi  8575  domunsncan  9075  pssnn  9163  findcard3  9253  ordtypelem7  9496  inf3lem5  9611  r1tr  9758  cardmin2  10004  ac10ct  10037  isf32lem12  10366  isfin1-3  10388  fin17  10396  fin1a2s  10416  axdc4lem  10457  axcclem  10459  ttukeylem2  10512  genpcd  11015  ltexprlem3  11047  prlem936  11056  supsrlem  11120  mul0or  11878  un0addcl  12561  un0mulcl  12562  btwnnz  12697  uznfz  13665  elfz0ubfz0  13687  elfzo0z  13757  fzofzim  13765  ssfzoulel  13816  ssfzo12bi  13817  fzoopth  13818  subfzo0  13849  modmuladdim  13978  modaddmodup  13998  modfzo0difsn  14007  axdc4uzlem  14047  expaddz  14170  sq01  14289  hashnn0n0nn  14455  hashss  14473  hashgt12el  14487  fi1uzind  14572  brfi1indALT  14575  ccatalpha  14660  swrdswrdlem  14773  swrdswrd  14774  swrdccatin1  14794  pfxccatin12lem3  14801  repswswrd  14855  cshf1  14881  cshw1  14893  2cshwcshw  14896  sqrmo  15338  caubnd2  15445  summo  15803  nno  16472  divalglem8  16490  lcmdvds  16698  lcmfunsnlem1  16727  hashgcdeq  16881  modprm0  16897  pcqcl  16948  vdwnnlem3  17089  prmgaplem5  17147  prmgaplem7  17149  catpropd  17797  cicsym  17893  isinitoi  18088  istermoi  18089  iszeroi  18098  acsfiindd  18641  tsrlemax  18674  0gisid  18761  issubg4  19269  gsmsymgreqlem2  19558  oddvdsnn0  19671  oddvds  19674  gexdvds  19711  lt6abl  20022  pgpfac1lem3  20206  01eq0ring  20691  unichnlidl  21425  isphld  21867  psdmul  22394  coe1ae0  22441  mdetdiaglem  22820  slesolex  22907  pmatcoe1fsupp  22926  cpmatelimp  22937  cpmatelimp2  22939  cpmatmcllem  22943  pm2mpf1  23024  mp2pm2mplem4  23034  fvmptnn04ifa  23075  fvmptnn04ifd  23078  chfacfscmul0  23083  chfacfpmmul0  23087  neii1  23331  neii2  23333  uncmp  23628  isfild  24084  fbunfip  24095  fgss2  24100  fgcl  24104  isufil2  24134  cfinufil  24154  ufilen  24156  fsumcn  25098  lmmbr  25486  iscau4  25507  caussi  25525  cmslssbn  25600  ovoliunnul  25735  ovolicc2lem4  25748  itg1ge0a  25939  rolle  26217  ulmcaulem  26630  cxpge0  26920  fsumvma  27449  gausslemma2dlem1a  27601  2sqb  27668  2sq2  27669  pntrsumbnd2  27803  pntlem3  27845  nofv  27893  ltsres  27898  muls0ord  28450  axeuclid  29420  axcontlem2  29422  usgrislfuspgr  29647  nbuhgr2vtx1edgblem  29811  usgredgsscusgredg  29919  upgrwlkvtxedg  30104  uspgr2wlkeq  30105  cyclnspth  30268  uspgrn2crct  30276  crctcshwlkn0lem4  30281  wlkiswwlks2lem5  30341  wlknewwlksn  30355  usgrwwlks2on  30426  umgrwwlks2on  30427  clwwlkccatlem  30459  clwlkclwwlklem2a4  30467  clwlkclwwlklem2a  30468  clwwisshclwwslemlem  30483  clwwlkel  30516  wwlksubclwwlk  30528  clwwlknon1  30567  clwwlknonex2lem2  30578  uhgr3cyclexlem  30661  vdgn1frgrv3  30777  2wspmdisj  30817  frgrregord013  30875  spansncvi  32133  lnconi  32514  cdj3lem1  32915  constrsqrtcl  34289  metider  34404  onvf1odlem4  35703  gonar  35974  goalr  35976  satffunlem2lem1  35983  finminlem  36937  clsint2  36948  cgsex2gd  37889  bj-finsumval0  38037  finxpsuclem  38151  pibt2  38171  wl-exeq  38297  phpreu  38358  poimirlem26  38395  poimir  38402  ismtyima  38553  elpaddn0  40673  tendospcanN  41896  nnproddivdvdsd  42866  dvdsexpnn0  43209  sn-remul0ord  43283  rexzrexnn0  43645  unxpwdom3  43936  unielss  44059  onov0suclim  44115  fsovrfovd  44849  radcnvrat  45138  2reu8i  48001  zm1nn  48190  subsubelfzo0  48215  2ffzoeq  48216  nnmul2  48218  fargshiftf  48340  2pwp1prm  48492  lighneal  48514  isuspgrimlem  48811  upgrimpths  48825  clnbgr3stgrgrlim  48935  gpgedgvtx0  48977  gpgedgvtx1  48978  isassintop  49125  uzlidlring  49150  2zrngamgm  49160  ply1mulgsumlem1  49316  suppdm  49440  rrxsphere  49678  inlinecirc02plem  49716  pgindnf  50642