Theorem impancom 456

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

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 401

This theorem is used by:  mo4  2593  spc2ed  3559  rexraleqim  3605  disjiun  5096  disjord  5097  disjiund  5099  propeqop  5489  euotd  5495  pwssun  5552  iotan0  6526  funopsn  7144  funopsnOLD  7145  isotr  7334  funeldmb  7359  resf1extb  7929  funfv1st2nd  8041  funelss  8042  el2mpocsbcl  8078  ressuppssdif  8179  oeordi  8571  domunsncan  9063  pssnn  9151  findcard3  9241  ordtypelem7  9484  inf3lem5  9599  r1tr  9746  cardmin2  9992  ac10ct  10025  isf32lem12  10354  isfin1-3  10376  fin17  10384  fin1a2s  10404  axdc4lem  10445  axcclem  10447  ttukeylem2  10500  genpcd  10997  ltexprlem3  11029  prlem936  11038  supsrlem  11102  mul0or  11860  un0addcl  12543  un0mulcl  12544  btwnnz  12678  uznfz  13645  elfz0ubfz0  13667  elfzo0z  13737  fzofzim  13745  ssfzoulel  13796  ssfzo12bi  13797  fzoopth  13798  subfzo0  13828  modmuladdim  13957  modaddmodup  13977  modfzo0difsn  13986  axdc4uzlem  14026  expaddz  14149  sq01  14268  hashnn0n0nn  14434  hashss  14452  hashgt12el  14466  fi1uzind  14551  brfi1indALT  14554  ccatalpha  14638  swrdswrdlem  14748  swrdswrd  14749  swrdccatin1  14769  pfxccatin12lem3  14776  repswswrd  14828  cshf1  14854  cshw1  14866  2cshwcshw  14869  sqrmo  15309  caubnd2  15416  summo  15775  nno  16446  divalglem8  16464  lcmdvds  16672  lcmfunsnlem1  16701  hashgcdeq  16855  modprm0  16871  pcqcl  16922  vdwnnlem3  17063  prmgaplem5  17121  prmgaplem7  17123  catpropd  17771  cicsym  17867  isinitoi  18062  istermoi  18063  iszeroi  18072  acsfiindd  18615  tsrlemax  18648  issubg4  19218  gsmsymgreqlem2  19507  oddvdsnn0  19620  oddvds  19623  gexdvds  19660  lt6abl  19971  pgpfac1lem3  20155  01eq0ring  20639  unichnlidl  21373  isphld  21815  psdmul  22340  coe1ae0  22387  mdetdiaglem  22766  slesolex  22850  pmatcoe1fsupp  22869  cpmatelimp  22880  cpmatelimp2  22882  cpmatmcllem  22886  pm2mpf1  22967  mp2pm2mplem4  22977  fvmptnn04ifa  23018  fvmptnn04ifd  23021  chfacfscmul0  23026  chfacfpmmul0  23030  neii1  23274  neii2  23276  uncmp  23571  isfild  24026  fbunfip  24037  fgss2  24042  fgcl  24046  isufil2  24076  cfinufil  24096  ufilen  24098  fsumcn  25040  lmmbr  25428  iscau4  25449  caussi  25467  cmslssbn  25542  ovoliunnul  25677  ovolicc2lem4  25690  itg1ge0a  25881  rolle  26160  ulmcaulem  26568  cxpge0  26859  fsumvma  27388  gausslemma2dlem1a  27540  2sqb  27607  2sq2  27608  pntrsumbnd2  27742  pntlem3  27784  nofv  27832  ltsres  27837  muls0ord  28389  axeuclid  29324  axcontlem2  29326  usgrislfuspgr  29548  nbuhgr2vtx1edgblem  29712  usgredgsscusgredg  29820  upgrwlkvtxedg  30005  uspgr2wlkeq  30006  cyclnspth  30161  uspgrn2crct  30168  crctcshwlkn0lem4  30173  wlkiswwlks2lem5  30233  wlknewwlksn  30247  usgrwwlks2on  30318  umgrwwlks2on  30319  clwwlkccatlem  30351  clwlkclwwlklem2a4  30359  clwlkclwwlklem2a  30360  clwwisshclwwslemlem  30375  clwwlkel  30408  wwlksubclwwlk  30420  clwwlknon1  30459  clwwlknonex2lem2  30470  uhgr3cyclexlem  30543  vdgn1frgrv3  30659  2wspmdisj  30699  frgrregord013  30757  spansncvi  32015  lnconi  32396  cdj3lem1  32797  constrsqrtcl  34178  metider  34293  prsrcmpltd  35479  onvf1odlem4  35598  gonar  35895  goalr  35897  satffunlem2lem1  35904  finminlem  36857  clsint2  36868  cgsex2gd  37809  bj-finsumval0  37957  finxpsuclem  38071  pibt2  38091  wl-exeq  38217  phpreu  38283  poimirlem26  38325  poimir  38332  ismtyima  38482  elpaddn0  40602  tendospcanN  41825  nnproddivdvdsd  42795  dvdsexpnn0  43123  sn-remul0ord  43197  rexzrexnn0  43559  unxpwdom3  43850  unielss  43973  onov0suclim  44029  fsovrfovd  44763  radcnvrat  45052  2reu8i  47878  zm1nn  48067  subsubelfzo0  48092  2ffzoeq  48093  nnmul2  48095  fargshiftf  48217  2pwp1prm  48369  lighneal  48391  isuspgrimlem  48688  upgrimpths  48702  clnbgr3stgrgrlim  48812  gpgedgvtx0  48854  gpgedgvtx1  48855  isassintop  49003  uzlidlring  49028  2zrngamgm  49038  ply1mulgsumlem1  49194  suppdm  49318  rrxsphere  49556  inlinecirc02plem  49594  pgindnf  50522