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  4481  fri  4536  ordelord  4595  tz7.7  4599  reusv3  4722  onint  4766  limsssuc  4821  tfindsg  4831  findsg  4863  dfimafn  5766  funimass4  5768  funimass3  5837  isomin  6048  isopolem  6056  smores2  6607  tfrlem1  6627  tfrlem9  6637  tz7.49  6693  oecl  6772  oaordi  6780  oaass  6795  omordi  6800  odi  6813  oen0  6820  nnaordi  6852  nnmordi  6865  php3  7284  domunfican  7370  dfac5  7998  cofsmo  8138  cfcoflem  8141  zorn2lem7  8371  tskwun  8648  mulcanpi  8766  ltexprlem7  8908  sup3  9954  elnnz  10281  irradd  10587  irrmul  10588  uzindi  11308  sqlecan  11475  unbenlem  13264  infpnlem1  13266  iscatd  13886  dirtr  14669  psrbaglefi  16425  isphld  16873  tgcl  17022  neindisj2  17175  bwth  17461  2ndcdisj  17507  fgcl  17898  rnelfm  17973  alexsubALTlem3  18068  usgrares1  21412  usgrafis  21417  nbgraf1olem5  21443  nbcusgra  21460  cusgrares  21469  cusgrasize  21475  usgrnloop  21551  pthdepisspth  21562  fargshiftfva  21614  usgrcyclnl2  21616  eupatrl  21678  rngoueqz  22006  mdexchi  23826  atomli  23873  mdsymlem5  23898  sumdmdlem  23909  dfimafnf  24031  dfon2lem6  25399  predpo  25439  btwnconn1lem11  25979  itg2addnc  26205  finminlem  26258  dmncan1  26623  eldioph2  26757  funressnfv  27906  dfaimafn  27943  otiunsndisj  28002  otiunsndisjX  28003  elfzonelfzo  28044  swrdnd  28074  swrdccat3  28104  swrdccat3b  28106  2shwrd  28146  shwrdeqdif2s  28157  usgra2wlkspth  28182  usgra2pthlem1  28184  usgra2adedgspthlem2  28188  el2spthonot  28211  2spontn0vne  28228  frgra3vlem1  28248  3vfriswmgralem  28252  vdgn0frgrav2  28273  vdgn1frgrav2  28275  frgrancvvdeqlemC  28286  frgrancvvdgeq  28290  frgrawopreglem5  28295  frg2woteq  28307  usg2spot2nb  28312  2spotmdisj  28315  bnj517  29110  bnj1118  29207  lshpdisj  29624  2at0mat0  30161  llncvrlpln2  30193  lplncvrlvol2  30251  lhpexle2lem  30645  cdlemk33N  31545  cdlemk34  31546
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