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 416 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 86 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
43imp 410 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  mo4  2649  eqrdav  2821  spc2ed  3577  rexraleqim  3615  disjiun  5029  disjord  5030  disjiund  5032  propeqop  5374  euotd  5380  pwssun  5433  iotan0  6324  funopsn  6892  isotr  7073  funfv1st2nd  7731  funelss  7732  el2mpocsbcl  7767  ressuppssdif  7838  oeordi  8200  domunsncan  8604  pssnn  8724  findcard3  8749  ordtypelem7  8976  inf3lem5  9083  r1tr  9193  cardmin2  9416  ac10ct  9449  isf32lem12  9775  isfin1-3  9797  fin17  9805  fin1a2s  9825  axdc4lem  9866  axcclem  9868  ttukeylem2  9921  genpcd  10417  ltexprlem3  10449  prlem936  10458  supsrlem  10522  mul0or  11269  un0addcl  11918  un0mulcl  11919  btwnnz  12046  uznfz  12985  elfz0ubfz0  13006  elfzo0z  13074  fzofzim  13079  ssfzoulel  13126  ssfzo12bi  13127  subfzo0  13154  modmuladdim  13277  modaddmodup  13297  modfzo0difsn  13306  axdc4uzlem  13346  expaddz  13469  sq01  13582  hashnn0n0nn  13748  hashss  13766  hashgt12el  13779  fi1uzind  13851  brfi1indALT  13854  ccatalpha  13938  swrdswrdlem  14057  swrdswrd  14058  swrdccatin1  14078  pfxccatin12lem3  14085  repswswrd  14137  cshf1  14163  cshw1  14175  2cshwcshw  14178  sqrmo  14602  caubnd2  14708  summo  15065  nno  15722  divalglem8  15740  lcmdvds  15941  lcmfunsnlem1  15970  hashgcdeq  16115  modprm0  16131  pcqcl  16182  vdwnnlem3  16322  prmgaplem5  16380  prmgaplem7  16382  catpropd  16970  cicsym  17065  isinitoi  17254  istermoi  17255  iszeroi  17260  acsfiindd  17778  tsrlemax  17821  issubg4  18289  gsmsymgreqlem2  18550  oddvdsnn0  18663  oddvds  18666  gexdvds  18700  lt6abl  19006  pgpfac1lem3  19190  isphld  20341  coe1ae0  20843  mdetdiaglem  21201  slesolex  21285  pmatcoe1fsupp  21304  cpmatelimp  21315  cpmatelimp2  21317  cpmatmcllem  21321  pm2mpf1  21402  mp2pm2mplem4  21412  fvmptnn04ifa  21453  fvmptnn04ifd  21456  chfacfscmul0  21461  chfacfpmmul0  21465  neii1  21709  neii2  21711  uncmp  22006  isfild  22461  fbunfip  22472  fgss2  22477  fgcl  22481  isufil2  22511  cfinufil  22531  ufilen  22533  fsumcn  23473  lmmbr  23860  iscau4  23881  caussi  23899  cmslssbn  23974  ovoliunnul  24109  ovolicc2lem4  24122  itg1ge0a  24313  rolle  24591  ulmcaulem  24987  cxpge0  25272  fsumvma  25795  gausslemma2dlem1a  25947  2sqb  26014  2sq2  26015  pntrsumbnd2  26149  pntlem3  26191  axeuclid  26755  axcontlem2  26757  usgrislfuspgr  26975  nbuhgr2vtx1edgblem  27139  usgredgsscusgredg  27247  upgrwlkvtxedg  27432  uspgr2wlkeq  27433  cyclnspth  27587  uspgrn2crct  27592  crctcshwlkn0lem4  27597  wlkiswwlks2lem5  27657  wlknewwlksn  27671  umgrwwlks2on  27741  clwwlkccatlem  27772  clwlkclwwlklem2a4  27780  clwlkclwwlklem2a  27781  clwwisshclwwslemlem  27796  clwwlkel  27829  wwlksubclwwlk  27841  clwwlknon1  27880  clwwlknonex2lem2  27891  uhgr3cyclexlem  27964  vdgn1frgrv3  28080  2wspmdisj  28120  frgrregord013  28178  spansncvi  29433  lnconi  29814  cdj3lem1  30215  metider  31211  prsrcmpltd  32421  gonar  32716  goalr  32718  satffunlem2lem1  32725  funeldmb  33080  nofv  33238  sltres  33243  finminlem  33740  clsint2  33751  bj-finsumval0  34661  finxpsuclem  34775  pibt2  34795  wl-exeq  34897  phpreu  34999  poimirlem26  35041  poimir  35048  ismtyima  35199  elpaddn0  37054  tendospcanN  38277  nnproddivdvdsd  39250  rexzrexnn0  39675  unxpwdom3  39969  fsovrfovd  40641  radcnvrat  40952  2reu8i  43608  zm1nn  43798  subsubelfzo0  43822  fzoopth  43823  2ffzoeq  43824  fargshiftf  43896  2pwp1prm  44045  lighneal  44068  isomuspgrlem1  44284  isassintop  44409  uzlidlring  44492  2zrngamgm  44502  ply1mulgsumlem1  44733  suppdm  44858  rrxsphere  45101  inlinecirc02plem  45139
  Copyright terms: Public domain W3C validator