MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impancom Structured version   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  1956  eqrdav  2434  disjiun  4194  euotd  4449  pwssun  4481  isotr  6048  oeordi  6822  domunsncan  7200  pssnn  7319  findcard3  7342  ordtypelem7  7485  inf3lem5  7579  r1tr  7694  cardmin2  7877  ac10ct  7907  isf32lem12  8236  isfin1-3  8258  fin17  8266  fin1a2s  8286  axdc4lem  8327  axcclem  8329  ttukeylem2  8382  genpcd  8875  ltexprlem3  8907  prlem936  8916  supsrlem  8978  mul0or  9654  un0addcl  10245  un0mulcl  10246  btwnnz  10338  uznfz  11122  axdc4uzlem  11313  expaddz  11416  sq01  11493  hashnn0n0nn  11656  hashgt12el  11674  brfi1uzind  11707  sqrmo  12049  caubnd2  12153  summo  12503  divalglem8  12912  pcqcl  13222  vdwnnlem3  13357  catpropd  13927  acsfiindd  14595  tsrlemax  14644  issubg4  14953  oddvdsnn0  15174  oddvds  15177  gexdvds  15210  lt6abl  15496  pgpfac1lem3  15627  isphld  16877  neii1  17162  neii2  17164  uncmp  17458  isfild  17882  fbunfip  17893  fgss2  17898  fgcl  17902  isufil2  17932  cfinufil  17952  ufilen  17954  fsumcn  18892  lmmbr  19203  iscau4  19224  caussi  19242  ovoliunnul  19395  ovolicc2lem4  19408  itg1ge0a  19595  rolle  19866  ulmcaulem  20302  cxpge0  20566  fsumvma  20989  2sqb  21154  pntrsumbnd2  21253  pntlem3  21295  nbcusgra  21464  cusgrares  21473  usgrasscusgra  21484  sizeusglecusglem1  21485  usgrnloop  21555  wlkdvspthlem  21599  fargshiftf  21615  ghgrp  21948  ghablo  21949  spansncvi  23146  lnconi  23528  cdj3lem1  23929  metider  24281  ghomf1olem  25097  nofv  25604  sltres  25611  axeuclid  25894  axcontlem2  25896  wl-exeq  26226  finminlem  26312  clsint2  26323  ismtyima  26503  rexzrexnn0  26855  unxpwdom3  27224  hashgcdeq  27485  elfzelfzelfz  28093  subsubelfzo0  28118  swrdvalodmlem1  28159  swrdswrdlem  28164  swrdswrd  28165  swrdccatin1  28171  swrdccatin12lem4  28179  modprm0  28194  cshw1  28238  cshwsame  28240  usgra2pthspth  28258  usgra2wlkspthlem2  28260  usg2spthonot0  28309  frgrancvvdeqlem3  28358  frgrancvvdeqlem4  28359  spimtNEW7  29444  elpaddn0  30534  tendospcanN  31758
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