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

Theorem imp31 421
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 418 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 418 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  imp41  576  imp5d  582  impl  603  anassrs  629  an31s  781  3imp  1146  3expa  1152  pwssun  4402  fri  4458  ordelord  4517  tz7.7  4521  reusv3  4645  onint  4689  limsssuc  4744  tfindsg  4754  findsg  4786  dfimafn  5678  funimass4  5680  funimass3  5748  isomin  5957  isopolem  5965  smores2  6513  tfrlem1  6533  tfrlem9  6543  tz7.49  6599  oecl  6678  oaordi  6686  oaass  6701  omordi  6706  odi  6719  oen0  6726  nnaordi  6758  nnmordi  6771  php3  7190  domunfican  7276  dfac5  7902  cofsmo  8042  cfcoflem  8045  zorn2lem7  8276  tskwun  8553  mulcanpi  8671  ltexprlem7  8813  sup3  9858  elnnz  10185  irradd  10491  irrmul  10492  uzindi  11207  sqlecan  11374  unbenlem  13163  infpnlem1  13165  iscatd  13785  dirtr  14568  psrbaglefi  16328  isphld  16775  tgcl  16924  neindisj2  17077  2ndcdisj  17399  fgcl  17786  rnelfm  17861  alexsubALTlem3  17956  usgrares1  21094  usgrafis  21099  rngoueqz  21408  mdexchi  23228  atomli  23275  mdsymlem5  23300  sumdmdlem  23311  dfimafnf  23446  dfon2lem6  24885  predpo  24925  btwnconn1lem11  25462  itg2addnc  25677  finminlem  25738  dmncan1  26207  eldioph2  26347  funressnfv  27499  dfaimafn  27536  nbgraf1olem5  27611  nbcusgra  27628  cusgrares  27637  cusgrasize  27643  usgrnloop  27709  pthdepisspth  27718  fargshiftfva  27764  eupatrl  27765  usgrcyclnl2  27767  frgra3vlem1  27835  3vfriswmgralem  27839  vdgn0frgrav2  27860  vdgn1frgrav2  27862  frgrancvvdeqlemC  27874  frgrancvvdgeq  27878  frgrawopreglem5  27883  bnj517  28681  bnj1118  28778  lshpdisj  29248  2at0mat0  29785  llncvrlpln2  29817  lplncvrlvol2  29875  lhpexle2lem  30269  cdlemk33N  31169  cdlemk34  31170
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