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

Theorem impancom 452
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 413 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 86 . 2 (𝜑 → (𝜒 → (𝜓𝜃)))
43imp 407 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  mo4  2646  eqrdav  2820  spc2ed  3601  rexraleqim  3639  disjiun  5045  disjord  5046  disjiund  5048  propeqop  5389  euotd  5395  pwssun  5449  iotan0  6339  funopsn  6903  isotr  7078  funfv1st2nd  7736  funelss  7737  el2mpocsbcl  7771  ressuppssdif  7842  oeordi  8203  domunsncan  8606  pssnn  8725  findcard3  8750  ordtypelem7  8977  inf3lem5  9084  r1tr  9194  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  fiminreOLD  11579  un0addcl  11919  un0mulcl  11920  btwnnz  12047  uznfz  12980  elfz0ubfz0  13001  elfzo0z  13069  fzofzim  13074  ssfzoulel  13121  ssfzo12bi  13122  subfzo0  13149  modmuladdim  13272  modaddmodup  13292  modfzo0difsn  13301  axdc4uzlem  13341  expaddz  13463  sq01  13576  hashnn0n0nn  13742  hashss  13760  hashgt12el  13773  fi1uzind  13845  brfi1indALT  13848  ccatalpha  13937  swrdswrdlem  14056  swrdswrd  14057  swrdccatin1  14077  pfxccatin12lem3  14084  repswswrd  14136  cshf1  14162  cshw1  14174  2cshwcshw  14177  sqrmo  14601  caubnd2  14707  summo  15064  nno  15723  divalglem8  15741  lcmdvds  15942  lcmfunsnlem1  15971  hashgcdeq  16116  modprm0  16132  pcqcl  16183  vdwnnlem3  16323  prmgaplem5  16381  prmgaplem7  16383  catpropd  16969  cicsym  17064  isinitoi  17253  istermoi  17254  iszeroi  17259  acsfiindd  17777  tsrlemax  17820  issubg4  18238  gsmsymgreqlem2  18490  oddvdsnn0  18603  oddvds  18606  gexdvds  18640  lt6abl  18946  pgpfac1lem3  19130  coe1ae0  20314  isphld  20728  mdetdiaglem  21137  slesolex  21221  pmatcoe1fsupp  21239  cpmatelimp  21250  cpmatelimp2  21252  cpmatmcllem  21256  pm2mpf1  21337  mp2pm2mplem4  21347  fvmptnn04ifa  21388  fvmptnn04ifd  21391  chfacfscmul0  21396  chfacfpmmul0  21400  neii1  21644  neii2  21646  uncmp  21941  isfild  22396  fbunfip  22407  fgss2  22412  fgcl  22416  isufil2  22446  cfinufil  22466  ufilen  22468  fsumcn  23407  lmmbr  23790  iscau4  23811  caussi  23829  cmslssbn  23904  ovoliunnul  24037  ovolicc2lem4  24050  itg1ge0a  24241  rolle  24516  ulmcaulem  24911  cxpge0  25193  fsumvma  25717  gausslemma2dlem1a  25869  2sqb  25936  2sq2  25937  pntrsumbnd2  26071  pntlem3  26113  axeuclid  26677  axcontlem2  26679  usgrislfuspgr  26897  nbuhgr2vtx1edgblem  27061  usgredgsscusgredg  27169  upgrwlkvtxedg  27354  uspgr2wlkeq  27355  cyclnspth  27509  uspgrn2crct  27514  crctcshwlkn0lem4  27519  wlkiswwlks2lem5  27579  wlknewwlksn  27593  umgrwwlks2on  27664  clwwlkccatlem  27695  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwwisshclwwslemlem  27719  clwwlkel  27753  wwlksubclwwlk  27765  clwwlknon1  27804  clwwlknonex2lem2  27815  uhgr3cyclexlem  27888  vdgn1frgrv3  28004  2wspmdisj  28044  frgrregord013  28102  spansncvi  29357  lnconi  29738  cdj3lem1  30139  metider  31034  prsrcmpltd  32245  gonar  32540  goalr  32542  satffunlem2lem1  32549  funeldmb  32904  nofv  33062  sltres  33067  finminlem  33564  clsint2  33575  bj-finsumval0  34456  finxpsuclem  34561  pibt2  34581  wl-exeq  34656  phpreu  34758  poimirlem26  34800  poimir  34807  ismtyima  34964  elpaddn0  36818  tendospcanN  38041  rexzrexnn0  39281  unxpwdom3  39575  fsovrfovd  40235  radcnvrat  40526  2reu8i  43193  zm1nn  43383  subsubelfzo0  43407  fzoopth  43408  2ffzoeq  43409  fargshiftf  43447  2pwp1prm  43598  lighneal  43623  isomuspgrlem1  43839  isassintop  44015  uzlidlring  44098  2zrngamgm  44108  ply1mulgsumlem1  44338  suppdm  44463  rrxsphere  44633  inlinecirc02plem  44671
  Copyright terms: Public domain W3C validator