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  4298  fri  4354  ordelord  4413  tz7.7  4417  reusv3  4541  onint  4585  limsssuc  4640  tfindsg  4650  findsg  4682  dfimafn  5533  funimass4  5535  funimass3  5603  isomin  5796  isopolem  5804  smores2  6367  tfrlem1  6387  tfrlem9  6397  tz7.49  6453  oecl  6532  oaordi  6540  oaass  6555  omordi  6560  odi  6573  oen0  6580  nnaordi  6612  nnmordi  6625  php3  7043  domunfican  7125  dfac5  7751  cofsmo  7891  cfcoflem  7894  zorn2lem7  8125  tskwun  8402  mulcanpi  8520  ltexprlem7  8662  sup3  9707  elnnz  10030  irradd  10336  irrmul  10337  uzindi  11039  sqlecan  11205  unbenlem  12951  infpnlem1  12953  iscatd  13571  dirtr  14354  psrbaglefi  16114  isphld  16554  tgcl  16703  neindisj2  16856  2ndcdisj  17178  fgcl  17569  rnelfm  17644  alexsubALTlem3  17739  rngoueqz  21091  mdexchi  22911  atomli  22958  mdsymlem5  22983  sumdmdlem  22994  dfimafnf  23037  dfon2lem6  23548  predpo  23588  btwnconn1lem11  24130  trooo  24805  trinv  24806  ltrooo  24815  truni1  24916  osneisi  24942  cmptdst  24979  bwt2  25003  lvsovso  25037  supexr  25042  addidv2  25068  icccon2  25111  cmpmon  25226  icmpmon  25227  idsubfun  25269  eltintpar  25310  finminlem  25642  dmncan1  26112  eldioph2  26252  funressnfv  27382  dfaimafn  27418  bnj517  28196  bnj1118  28293  lshpdisj  28456  2at0mat0  28993  llncvrlpln2  29025  lplncvrlvol2  29083  lhpexle2lem  29477  cdlemk33N  30377  cdlemk34  30378
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