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

Theorem impancom 427
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 423 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32com23 72 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
43imp 418 1  |-  ( (
ph  /\  ch )  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  spimt  1927  eqrdav  2295  disjiun  4029  euotd  4283  pwssun  4315  isotr  5849  oeordi  6601  domunsncan  6978  pssnn  7097  findcard3  7116  ordtypelem7  7255  inf3lem5  7349  r1tr  7464  cardmin2  7647  ac10ct  7677  isf32lem12  8006  isfin1-3  8028  fin17  8036  fin1a2s  8056  axdc4lem  8097  axcclem  8099  ttukeylem2  8153  genpcd  8646  ltexprlem3  8678  prlem936  8687  supsrlem  8749  mul0or  9424  un0addcl  10013  un0mulcl  10014  btwnnz  10104  uznfz  10881  axdc4uzlem  11060  expaddz  11162  sq01  11239  sqrmo  11753  caubnd2  11857  summo  12206  divalglem8  12615  pcqcl  12925  vdwnnlem3  13060  catpropd  13628  acsfiindd  14296  tsrlemax  14345  issubg4  14654  oddvdsnn0  14875  oddvds  14878  gexdvds  14911  lt6abl  15197  pgpfac1lem3  15328  isphld  16574  neii1  16859  neii2  16861  uncmp  17146  isfild  17569  fbunfip  17580  fgss2  17585  fgcl  17589  isufil2  17619  cfinufil  17639  ufilen  17641  fsumcn  18390  lmmbr  18700  iscau4  18721  caussi  18739  ovoliunnul  18882  ovolicc2lem4  18895  itg1ge0a  19082  rolle  19353  ulmcaulem  19787  cxpge0  20046  fsumvma  20468  2sqb  20633  pntrsumbnd2  20732  pntlem3  20774  ghgrp  21051  ghablo  21052  spansncvi  22247  lnconi  22629  cdj3lem1  23030  ghomf1olem  24016  nofv  24382  sltres  24389  axeuclid  24663  axcontlem2  24665  truni3  25610  iintlem1  25713  imonclem  25916  iepiclem  25926  pdiveql  26271  finminlem  26334  clsint2  26350  ismtyima  26630  rexzrexnn0  26988  unxpwdom3  27359  hashgcdeq  27620  rfcnnnub  27810  hashgt12el  28218  nbcusgra  28298  usgrnloop  28351  wlkdvspthlem  28365  fargshiftf  28381  spimtNEW7  29484  elpaddn0  30611  tendospcanN  31835
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 177  df-an 360
  Copyright terms: Public domain W3C validator