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

Theorem impancom 428
Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
Hypothesis
Ref Expression
impancom.1  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
Assertion
Ref Expression
impancom  |-  ( (
ph  /\  ch )  ->  ( ps  ->  th )
)

Proof of Theorem impancom
StepHypRef Expression
1 impancom.1 . . . 4  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
21ex 424 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 74 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
43imp 419 1  |-  ( (
ph  /\  ch )  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  spimtOLD  1954  eqrdav  2403  disjiun  4162  euotd  4417  pwssun  4449  isotr  6015  oeordi  6789  domunsncan  7167  pssnn  7286  findcard3  7309  ordtypelem7  7449  inf3lem5  7543  r1tr  7658  cardmin2  7841  ac10ct  7871  isf32lem12  8200  isfin1-3  8222  fin17  8230  fin1a2s  8250  axdc4lem  8291  axcclem  8293  ttukeylem2  8346  genpcd  8839  ltexprlem3  8871  prlem936  8880  supsrlem  8942  mul0or  9618  un0addcl  10209  un0mulcl  10210  btwnnz  10302  uznfz  11085  axdc4uzlem  11276  expaddz  11379  sq01  11456  hashnn0n0nn  11619  hashgt12el  11637  brfi1uzind  11670  sqrmo  12012  caubnd2  12116  summo  12466  divalglem8  12875  pcqcl  13185  vdwnnlem3  13320  catpropd  13890  acsfiindd  14558  tsrlemax  14607  issubg4  14916  oddvdsnn0  15137  oddvds  15140  gexdvds  15173  lt6abl  15459  pgpfac1lem3  15590  isphld  16840  neii1  17125  neii2  17127  uncmp  17420  isfild  17843  fbunfip  17854  fgss2  17859  fgcl  17863  isufil2  17893  cfinufil  17913  ufilen  17915  fsumcn  18853  lmmbr  19164  iscau4  19185  caussi  19203  ovoliunnul  19356  ovolicc2lem4  19369  itg1ge0a  19556  rolle  19827  ulmcaulem  20263  cxpge0  20527  fsumvma  20950  2sqb  21115  pntrsumbnd2  21214  pntlem3  21256  nbcusgra  21425  cusgrares  21434  usgrasscusgra  21445  sizeusglecusglem1  21446  usgrnloop  21516  wlkdvspthlem  21560  fargshiftf  21576  ghgrp  21909  ghablo  21910  spansncvi  23107  lnconi  23489  cdj3lem1  23890  metider  24242  ghomf1olem  25058  nofv  25525  sltres  25532  axeuclid  25806  axcontlem2  25808  finminlem  26211  clsint2  26222  ismtyima  26402  rexzrexnn0  26754  unxpwdom3  27124  hashgcdeq  27385  elfzelfzelfz  27981  swrdswrdlem  28010  swrdswrd  28011  swrdccatin1  28016  swrdccatin2  28018  swrdccat3b  28031  usgra2pthspth  28035  usgra2wlkspthlem2  28037  usg2spthonot0  28086  frgrancvvdeqlem3  28135  frgrancvvdeqlem4  28136  spimtNEW7  29213  elpaddn0  30282  tendospcanN  31506
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator