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  1914  eqrdav  2282  disjiun  4013  euotd  4267  pwssun  4299  isotr  5833  oeordi  6585  domunsncan  6962  pssnn  7081  findcard3  7100  ordtypelem7  7239  inf3lem5  7333  r1tr  7448  cardmin2  7631  ac10ct  7661  isf32lem12  7990  isfin1-3  8012  fin17  8020  fin1a2s  8040  axdc4lem  8081  axcclem  8083  ttukeylem2  8137  genpcd  8630  ltexprlem3  8662  prlem936  8671  supsrlem  8733  mul0or  9408  un0addcl  9997  un0mulcl  9998  btwnnz  10088  uznfz  10865  axdc4uzlem  11044  expaddz  11146  sq01  11223  sqrmo  11737  caubnd2  11841  summo  12190  divalglem8  12599  pcqcl  12909  vdwnnlem3  13044  catpropd  13612  acsfiindd  14280  tsrlemax  14329  issubg4  14638  oddvdsnn0  14859  oddvds  14862  gexdvds  14895  lt6abl  15181  pgpfac1lem3  15312  isphld  16558  neii1  16843  neii2  16845  uncmp  17130  isfild  17553  fbunfip  17564  fgss2  17569  fgcl  17573  isufil2  17603  cfinufil  17623  ufilen  17625  fsumcn  18374  lmmbr  18684  iscau4  18705  caussi  18723  ovoliunnul  18866  ovolicc2lem4  18879  itg1ge0a  19066  rolle  19337  ulmcaulem  19771  cxpge0  20030  fsumvma  20452  2sqb  20617  pntrsumbnd2  20716  pntlem3  20758  ghgrp  21035  ghablo  21036  spansncvi  22231  lnconi  22613  cdj3lem1  23014  ghomf1olem  24001  nofv  24311  sltres  24318  axeuclid  24591  axcontlem2  24593  truni3  25507  iintlem1  25610  imonclem  25813  iepiclem  25823  pdiveql  26168  finminlem  26231  clsint2  26247  ismtyima  26527  rexzrexnn0  26885  unxpwdom3  27256  hashgcdeq  27517  rfcnnnub  27707  nbcusgra  28159  elpaddn0  29989  tendospcanN  31213
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