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  1947  eqrdav  2388  disjiun  4145  euotd  4400  pwssun  4432  isotr  5997  oeordi  6768  domunsncan  7146  pssnn  7265  findcard3  7288  ordtypelem7  7428  inf3lem5  7522  r1tr  7637  cardmin2  7820  ac10ct  7850  isf32lem12  8179  isfin1-3  8201  fin17  8209  fin1a2s  8229  axdc4lem  8270  axcclem  8272  ttukeylem2  8325  genpcd  8818  ltexprlem3  8850  prlem936  8859  supsrlem  8921  mul0or  9596  un0addcl  10187  un0mulcl  10188  btwnnz  10280  uznfz  11062  axdc4uzlem  11250  expaddz  11353  sq01  11430  hashnn0n0nn  11593  hashgt12el  11611  brfi1uzind  11644  sqrmo  11986  caubnd2  12090  summo  12440  divalglem8  12849  pcqcl  13159  vdwnnlem3  13294  catpropd  13864  acsfiindd  14532  tsrlemax  14581  issubg4  14890  oddvdsnn0  15111  oddvds  15114  gexdvds  15147  lt6abl  15433  pgpfac1lem3  15564  isphld  16810  neii1  17095  neii2  17097  uncmp  17390  isfild  17813  fbunfip  17824  fgss2  17829  fgcl  17833  isufil2  17863  cfinufil  17883  ufilen  17885  fsumcn  18773  lmmbr  19084  iscau4  19105  caussi  19123  ovoliunnul  19272  ovolicc2lem4  19285  itg1ge0a  19472  rolle  19743  ulmcaulem  20179  cxpge0  20443  fsumvma  20866  2sqb  21031  pntrsumbnd2  21130  pntlem3  21172  nbcusgra  21340  cusgrares  21349  usgrasscusgra  21360  sizeusglecusglem1  21361  usgrnloop  21421  wlkdvspthlem  21457  fargshiftf  21473  ghgrp  21806  ghablo  21807  spansncvi  23004  lnconi  23386  cdj3lem1  23787  ghomf1olem  24886  nofv  25337  sltres  25344  axeuclid  25618  axcontlem2  25620  finminlem  26014  clsint2  26025  ismtyima  26205  rexzrexnn0  26557  unxpwdom3  26927  hashgcdeq  27188  frgrancvvdeqlem3  27786  frgrancvvdeqlem4  27787  spimtNEW7  28847  elpaddn0  29916  tendospcanN  31140
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