Theorem impancom 451

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mo4  2559  eqrdav  2728  spc2ed  3558  rexraleqim  3604  disjiun  5083  disjord  5084  disjiund  5086  propeqop  5454  euotd  5460  pwssun  5515  iotan0  6476  funopsn  7086  isotr  7277  funeldmb  7300  resf1extb  7874  funfv1st2nd  7988  funelss  7989  el2mpocsbcl  8025  ressuppssdif  8125  oeordi  8512  domunsncan  9001  pssnn  9092  findcard3  9187  findcard3OLD  9188  ordtypelem7  9435  inf3lem5  9547  r1tr  9691  cardmin2  9914  ac10ct  9947  isf32lem12  10277  isfin1-3  10299  fin17  10307  fin1a2s  10327  axdc4lem  10368  axcclem  10370  ttukeylem2  10423  genpcd  10919  ltexprlem3  10951  prlem936  10960  supsrlem  11024  mul0or  11779  un0addcl  12436  un0mulcl  12437  btwnnz  12571  uznfz  13532  elfz0ubfz0  13554  elfzo0z  13623  fzofzim  13631  ssfzoulel  13682  ssfzo12bi  13683  fzoopth  13684  subfzo0  13711  modmuladdim  13840  modaddmodup  13860  modfzo0difsn  13869  axdc4uzlem  13909  expaddz  14032  sq01  14151  hashnn0n0nn  14317  hashss  14335  hashgt12el  14348  fi1uzind  14433  brfi1indALT  14436  ccatalpha  14519  swrdswrdlem  14629  swrdswrd  14630  swrdccatin1  14650  pfxccatin12lem3  14657  repswswrd  14709  cshf1  14735  cshw1  14747  2cshwcshw  14751  sqrmo  15177  caubnd2  15284  summo  15643  nno  16312  divalglem8  16330  lcmdvds  16538  lcmfunsnlem1  16567  hashgcdeq  16720  modprm0  16736  pcqcl  16787  vdwnnlem3  16928  prmgaplem5  16986  prmgaplem7  16988  catpropd  17634  cicsym  17730  isinitoi  17925  istermoi  17926  iszeroi  17935  acsfiindd  18478  tsrlemax  18511  issubg4  19043  gsmsymgreqlem2  19329  oddvdsnn0  19442  oddvds  19445  gexdvds  19482  lt6abl  19793  pgpfac1lem3  19977  01eq0ring  20434  isphld  21580  psdmul  22070  coe1ae0  22118  mdetdiaglem  22502  slesolex  22586  pmatcoe1fsupp  22605  cpmatelimp  22616  cpmatelimp2  22618  cpmatmcllem  22622  pm2mpf1  22703  mp2pm2mplem4  22713  fvmptnn04ifa  22754  fvmptnn04ifd  22757  chfacfscmul0  22762  chfacfpmmul0  22766  neii1  23010  neii2  23012  uncmp  23307  isfild  23762  fbunfip  23773  fgss2  23778  fgcl  23782  isufil2  23812  cfinufil  23832  ufilen  23834  fsumcn  24778  lmmbr  25175  iscau4  25196  caussi  25214  cmslssbn  25289  ovoliunnul  25425  ovolicc2lem4  25438  itg1ge0a  25629  rolle  25911  ulmcaulem  26320  cxpge0  26609  fsumvma  27141  gausslemma2dlem1a  27293  2sqb  27360  2sq2  27361  pntrsumbnd2  27495  pntlem3  27537  nofv  27586  sltres  27591  muls0ord  28112  axeuclid  28927  axcontlem2  28929  usgrislfuspgr  29151  nbuhgr2vtx1edgblem  29315  usgredgsscusgredg  29424  upgrwlkvtxedg  29609  uspgr2wlkeq  29610  cyclnspth  29765  uspgrn2crct  29772  crctcshwlkn0lem4  29777  wlkiswwlks2lem5  29837  wlknewwlksn  29851  umgrwwlks2on  29921  clwwlkccatlem  29952  clwlkclwwlklem2a4  29960  clwlkclwwlklem2a  29961  clwwisshclwwslemlem  29976  clwwlkel  30009  wwlksubclwwlk  30021  clwwlknon1  30060  clwwlknonex2lem2  30071  uhgr3cyclexlem  30144  vdgn1frgrv3  30260  2wspmdisj  30300  frgrregord013  30358  spansncvi  31615  lnconi  31996  cdj3lem1  32397  constrsqrtcl  33765  metider  33880  prsrcmpltd  35067  onvf1odlem4  35098  gonar  35387  goalr  35389  satffunlem2lem1  35396  finminlem  36311  clsint2  36322  bj-finsumval0  37278  finxpsuclem  37390  pibt2  37410  wl-exeq  37527  phpreu  37603  poimirlem26  37645  poimir  37652  ismtyima  37802  elpaddn0  39799  tendospcanN  41022  nnproddivdvdsd  41993  dvdsexpnn0  42327  sn-remul0ord  42401  rexzrexnn0  42797  unxpwdom3  43088  unielss  43211  onov0suclim  43267  fsovrfovd  44002  radcnvrat  44307  2reu8i  47117  zm1nn  47306  subsubelfzo0  47330  2ffzoeq  47331  fargshiftf  47444  2pwp1prm  47593  lighneal  47615  isuspgrimlem  47899  upgrimpths  47913  clnbgr3stgrgrlim  48023  gpgedgvtx0  48065  gpgedgvtx1  48066  isassintop  48214  uzlidlring  48239  2zrngamgm  48249  ply1mulgsumlem1  48391  suppdm  48515  rrxsphere  48753  inlinecirc02plem  48791  pgindnf  49721