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

Theorem imp31 422
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
imp31  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem imp31
StepHypRef Expression
1 imp3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21imp 419 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 419 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  imp41  577  imp5d  583  impl  604  anassrs  630  an31s  782  3imp  1147  3expa  1153  pwssun  4449  fri  4504  ordelord  4563  tz7.7  4567  reusv3  4690  onint  4734  limsssuc  4789  tfindsg  4799  findsg  4831  dfimafn  5734  funimass4  5736  funimass3  5805  isomin  6016  isopolem  6024  smores2  6575  tfrlem1  6595  tfrlem9  6605  tz7.49  6661  oecl  6740  oaordi  6748  oaass  6763  omordi  6768  odi  6781  oen0  6788  nnaordi  6820  nnmordi  6833  php3  7252  domunfican  7338  dfac5  7965  cofsmo  8105  cfcoflem  8108  zorn2lem7  8338  tskwun  8615  mulcanpi  8733  ltexprlem7  8875  sup3  9921  elnnz  10248  irradd  10554  irrmul  10555  uzindi  11275  sqlecan  11442  unbenlem  13231  infpnlem1  13233  iscatd  13853  dirtr  14636  psrbaglefi  16392  isphld  16840  tgcl  16989  neindisj2  17142  2ndcdisj  17472  fgcl  17863  rnelfm  17938  alexsubALTlem3  18033  usgrares1  21377  usgrafis  21382  nbgraf1olem5  21408  nbcusgra  21425  cusgrares  21434  cusgrasize  21440  usgrnloop  21516  pthdepisspth  21527  fargshiftfva  21579  usgrcyclnl2  21581  eupatrl  21643  rngoueqz  21971  mdexchi  23791  atomli  23838  mdsymlem5  23863  sumdmdlem  23874  dfimafnf  23996  dfon2lem6  25358  predpo  25398  btwnconn1lem11  25935  itg2addnc  26158  finminlem  26211  dmncan1  26576  eldioph2  26710  funressnfv  27859  dfaimafn  27896  otiunsndisj  27954  otiunsndisjX  27955  elfzonelfzo  27992  swrdnd  28001  swrdccat3  28029  swrdccat3b  28031  usgra2wlkspth  28038  usgra2pthlem1  28040  usgra2adedgspthlem2  28044  el2spthonot  28067  2spontn0vne  28084  frgra3vlem1  28104  3vfriswmgralem  28108  vdgn0frgrav2  28129  vdgn1frgrav2  28131  frgrancvvdeqlemC  28142  frgrancvvdgeq  28146  frgrawopreglem5  28151  frg2woteq  28163  usg2spot2nb  28168  2spotmdisj  28171  bnj517  28962  bnj1118  29059  lshpdisj  29470  2at0mat0  30007  llncvrlpln2  30039  lplncvrlvol2  30097  lhpexle2lem  30491  cdlemk33N  31391  cdlemk34  31392
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