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  1145  3expa  1151  pwssun  4301  fri  4357  ordelord  4416  tz7.7  4420  reusv3  4544  onint  4588  limsssuc  4643  tfindsg  4653  findsg  4685  dfimafn  5573  funimass4  5575  funimass3  5643  isomin  5836  isopolem  5844  smores2  6373  tfrlem1  6393  tfrlem9  6403  tz7.49  6459  oecl  6538  oaordi  6546  oaass  6561  omordi  6566  odi  6579  oen0  6586  nnaordi  6618  nnmordi  6631  php3  7049  domunfican  7131  dfac5  7757  cofsmo  7897  cfcoflem  7900  zorn2lem7  8131  tskwun  8408  mulcanpi  8526  ltexprlem7  8668  sup3  9713  elnnz  10036  irradd  10342  irrmul  10343  uzindi  11045  sqlecan  11211  unbenlem  12957  infpnlem1  12959  iscatd  13577  dirtr  14360  psrbaglefi  16120  isphld  16560  tgcl  16709  neindisj2  16862  2ndcdisj  17184  fgcl  17575  rnelfm  17650  alexsubALTlem3  17745  rngoueqz  21099  mdexchi  22917  atomli  22964  mdsymlem5  22989  sumdmdlem  23000  dfimafnf  23043  dfon2lem6  24146  predpo  24186  btwnconn1lem11  24722  itg2addnc  24935  trooo  25405  trinv  25406  ltrooo  25415  truni1  25516  osneisi  25542  cmptdst  25579  bwt2  25603  lvsovso  25637  supexr  25642  addidv2  25668  icccon2  25711  cmpmon  25826  icmpmon  25827  idsubfun  25869  eltintpar  25910  finminlem  26242  dmncan1  26712  eldioph2  26852  funressnfv  28002  dfaimafn  28038  nbcusgra  28170  cusgrauvtx  28179  frgra3vlem1  28189  3vfriswmgralem  28193  bnj517  28990  bnj1118  29087  lshpdisj  29250  2at0mat0  29787  llncvrlpln2  29819  lplncvrlvol2  29877  lhpexle2lem  30271  cdlemk33N  31171  cdlemk34  31172
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