MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impancom Structured version   Visualization version   GIF version

Theorem impancom 455
Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
Hypothesis
Ref Expression
impancom.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
impancom ((𝜑𝜒) → (𝜓𝜃))

Proof of Theorem impancom
StepHypRef Expression
1 impancom.1 . . . 4 ((𝜑𝜓) → (𝜒𝜃))
21ex 449 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 86 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
43imp 444 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
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 197  df-an 385
This theorem is referenced by:  eqrdav  2759  rexraleqim  3467  disjiun  4792  disjord  4793  disjiund  4795  propeqop  5118  euotd  5123  pwssun  5170  funopsn  6577  isotr  6750  el2mpt2csbcl  7419  ressuppssdif  7485  oeordi  7838  domunsncan  8227  pssnn  8345  findcard3  8370  ordtypelem7  8596  inf3lem5  8704  r1tr  8814  cardmin2  9034  ac10ct  9067  isf32lem12  9398  isfin1-3  9420  fin17  9428  fin1a2s  9448  axdc4lem  9489  axcclem  9491  ttukeylem2  9544  genpcd  10040  ltexprlem3  10072  prlem936  10081  supsrlem  10144  mul0or  10879  fiminre  11184  un0addcl  11538  un0mulcl  11539  btwnnz  11665  uznfz  12636  elfz0ubfz0  12657  elfzo0z  12724  fzofzim  12729  elfzom1p1elfzo  12762  ssfzoulel  12776  ssfzo12bi  12777  subfzo0  12804  modmuladdim  12927  modaddmodup  12947  modfzo0difsn  12956  axdc4uzlem  12996  expaddz  13118  sq01  13200  hashnn0n0nn  13392  hashss  13409  hashgt12el  13422  fi1uzind  13491  brfi1indALT  13494  ccatalpha  13585  swrdswrdlem  13679  swrdswrd  13680  swrdccatin1  13703  swrdccatin12lem3  13710  repswswrd  13751  cshwmodn  13761  cshf1  13776  cshw1  13788  2cshwcshw  13791  sqrmo  14211  caubnd2  14316  summo  14667  nno  15320  divalglem8  15345  lcmdvds  15543  lcmfunsnlem1  15572  hashgcdeq  15716  modprm0  15732  pcqcl  15783  vdwnnlem3  15923  prmgaplem5  15981  prmgaplem7  15983  catpropd  16590  cicsym  16685  isinitoi  16874  istermoi  16875  iszeroi  16880  acsfiindd  17398  tsrlemax  17441  issubg4  17834  gsmsymgreqlem2  18071  oddvdsnn0  18183  oddvds  18186  gexdvds  18219  lt6abl  18516  pgpfac1lem3  18696  coe1ae0  19808  isphld  20221  mdetdiaglem  20626  slesolex  20710  pmatcoe1fsupp  20728  cpmatelimp  20739  cpmatelimp2  20741  cpmatmcllem  20745  pm2mpf1  20826  mp2pm2mplem4  20836  fvmptnn04ifa  20877  fvmptnn04ifd  20880  chfacfscmul0  20885  chfacfpmmul0  20889  neii1  21132  neii2  21134  uncmp  21428  isfild  21883  fbunfip  21894  fgss2  21899  fgcl  21903  isufil2  21933  cfinufil  21953  ufilen  21955  fsumcn  22894  lmmbr  23276  iscau4  23297  caussi  23315  ovoliunnul  23495  ovolicc2lem4  23508  itg1ge0a  23697  rolle  23972  ulmcaulem  24367  cxpge0  24649  fsumvma  25158  gausslemma2dlem1a  25310  2sqb  25377  pntrsumbnd2  25476  pntlem3  25518  axeuclid  26063  axcontlem2  26065  usgrislfuspgr  26299  nbuhgr2vtx1edgblem  26467  usgredgsscusgredg  26586  upgrwlkvtxedg  26772  uspgr2wlkeq  26773  cyclnspth  26927  uspgrn2crct  26932  crctcshwlkn0lem4  26937  wlkiswwlks2lem5  27003  wlknewwlksn  27017  wlkwwlksur  27027  umgrwwlks2on  27099  clwwlkccatlem  27133  clwwlkccat  27134  clwlkclwwlklem2a4  27141  clwlkclwwlklem2a  27142  clwwisshclwwslemlem  27157  clwwlkel  27196  wwlksubclwwlk  27210  clwlksfoclwwlkOLD  27238  clwwlknon1  27266  clwwlknonex2lem2  27278  uhgr3cyclexlem  27354  vdgn1frgrv3  27472  2wspmdisj  27512  frgrregord013  27584  spansncvi  28841  lnconi  29222  cdj3lem1  29623  spc2ed  29642  metider  30267  funeldmb  31989  nofv  32137  sltres  32142  finminlem  32639  clsint2  32651  bj-finsumval0  33476  finxpsuclem  33563  wl-exeq  33652  phpreu  33724  poimirlem26  33766  poimir  33773  ismtyima  33933  elpaddn0  35607  tendospcanN  36832  rexzrexnn0  37888  unxpwdom3  38185  fsovrfovd  38823  radcnvrat  39033  zm1nn  41844  subsubelfzo0  41864  fzoopth  41865  2ffzoeq  41866  fargshiftf  41904  2pwp1prm  42031  lighneal  42056  isassintop  42374  uzlidlring  42457  2zrngamgm  42467  ply1mulgsumlem1  42702  suppdm  42828
  Copyright terms: Public domain W3C validator