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  2650  rexraleqim  3359  disjiun  4672  disjord  4673  disjiund  4675  propeqop  4999  euotd  5004  pwssun  5049  funopsn  6453  isotr  6626  el2mpt2csbcl  7295  ressuppssdif  7361  oeordi  7712  domunsncan  8101  pssnn  8219  findcard3  8244  ordtypelem7  8470  inf3lem5  8567  r1tr  8677  cardmin2  8862  ac10ct  8895  isf32lem12  9224  isfin1-3  9246  fin17  9254  fin1a2s  9274  axdc4lem  9315  axcclem  9317  ttukeylem2  9370  genpcd  9866  ltexprlem3  9898  prlem936  9907  supsrlem  9970  mul0or  10705  fiminre  11010  un0addcl  11364  un0mulcl  11365  btwnnz  11491  uznfz  12461  elfz0ubfz0  12482  elfzo0z  12549  fzofzim  12554  elfzom1p1elfzo  12587  ssfzoulel  12602  ssfzo12bi  12603  subfzo0  12630  modmuladdim  12753  modaddmodup  12773  modfzo0difsn  12782  axdc4uzlem  12822  expaddz  12944  sq01  13026  hashnn0n0nn  13218  hashss  13235  hashgt12el  13248  fi1uzind  13317  brfi1indALT  13320  ccatalpha  13411  swrdswrdlem  13505  swrdswrd  13506  swrdccatin1  13529  swrdccatin12lem3  13536  repswswrd  13577  cshwmodn  13587  cshf1  13602  cshw1  13614  2cshwcshw  13617  sqrmo  14036  caubnd2  14141  summo  14492  nno  15145  divalglem8  15170  lcmdvds  15368  lcmfunsnlem1  15397  hashgcdeq  15541  modprm0  15557  pcqcl  15608  vdwnnlem3  15748  prmgaplem5  15806  prmgaplem7  15808  catpropd  16416  cicsym  16511  isinitoi  16700  istermoi  16701  iszeroi  16706  acsfiindd  17224  tsrlemax  17267  issubg4  17660  gsmsymgreqlem2  17897  oddvdsnn0  18009  oddvds  18012  gexdvds  18045  lt6abl  18342  pgpfac1lem3  18522  coe1ae0  19634  isphld  20047  mdetdiaglem  20452  slesolex  20536  pmatcoe1fsupp  20554  cpmatelimp  20565  cpmatelimp2  20567  cpmatmcllem  20571  pm2mpf1  20652  mp2pm2mplem4  20662  fvmptnn04ifa  20703  fvmptnn04ifd  20706  chfacfscmul0  20711  chfacfpmmul0  20715  neii1  20958  neii2  20960  uncmp  21254  isfild  21709  fbunfip  21720  fgss2  21725  fgcl  21729  isufil2  21759  cfinufil  21779  ufilen  21781  fsumcn  22720  lmmbr  23102  iscau4  23123  caussi  23141  ovoliunnul  23321  ovolicc2lem4  23334  itg1ge0a  23523  rolle  23798  ulmcaulem  24193  cxpge0  24474  fsumvma  24983  gausslemma2dlem1a  25135  2sqb  25202  pntrsumbnd2  25301  pntlem3  25343  axeuclid  25888  axcontlem2  25890  usgrislfuspgr  26124  nbuhgr2vtx1edgblem  26292  usgredgsscusgredg  26411  upgrwlkvtxedg  26597  uspgr2wlkeq  26598  cyclnspth  26751  uspgrn2crct  26756  crctcshwlkn0lem4  26761  wlkiswwlks2lem5  26827  wlknewwlksn  26841  wlkwwlksur  26851  umgrwwlks2on  26923  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwwisshclwwslemlem  26970  clwwlkel  27009  wwlksubclwwlk  27023  clwlksfoclwwlk  27050  clwwlknon1  27072  clwwlknonex2lem2  27083  uhgr3cyclexlem  27159  vdgn1frgrv3  27277  2wspmdisj  27317  clwwlkccatlem  27331  clwwlkccat  27332  frgrregord013  27382  spansncvi  28639  lnconi  29020  cdj3lem1  29421  spc2ed  29440  metider  30065  funeldmb  31787  nofv  31935  sltres  31940  finminlem  32437  clsint2  32449  bj-finsumval0  33277  finxpsuclem  33364  wl-exeq  33451  phpreu  33523  poimirlem26  33565  poimir  33572  ismtyima  33732  elpaddn0  35404  tendospcanN  36629  rexzrexnn0  37685  unxpwdom3  37982  fsovrfovd  38620  radcnvrat  38830  zm1nn  41641  subsubelfzo0  41661  fzoopth  41662  2ffzoeq  41663  fargshiftf  41701  2pwp1prm  41828  lighneal  41853  isassintop  42171  uzlidlring  42254  2zrngamgm  42264  ply1mulgsumlem1  42499  suppdm  42625
  Copyright terms: Public domain W3C validator