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

Theorem imp31 430
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 427 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 427 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  imp41  591  imp5d  597  impl  618  anassrs  646  an31s  804  3imp  1188  3expa  1194  reusv3  4645  otiunsndisj  4742  pwssun  4775  fri  4830  ordelord  4889  tz7.7  4893  dfimafn  5897  funimass4  5899  funimass3  5979  isomin  6208  isopolem  6216  onint  6603  limsssuc  6658  tfindsg  6668  findsg  6700  suppfnss  6917  smores2  7017  tfrlem9  7046  tz7.49  7102  oecl  7179  oaordi  7187  oaass  7202  omordi  7207  odi  7220  oen0  7227  nnaordi  7259  nnmordi  7272  php3  7696  domunfican  7785  dfac5  8500  cofsmo  8640  cfcoflem  8643  zorn2lem7  8873  tskwun  9151  mulcanpi  9267  ltexprlem7  9409  sup3  10495  elnnz  10870  irradd  11207  irrmul  11208  uzsubsubfz  11710  fzo1fzo0n0  11841  elincfzoext  11855  elfzonelfzo  11893  uzindi  12073  ssnn0fi  12076  sqlecan  12256  wrd2ind  12694  repswccat  12748  cshwlen  12761  cshwidxmod  12765  2cshwcshw  12784  unbenlem  14510  infpnlem1  14512  iscatd  15162  initoeu1  15489  termoeu1  15496  dirtr  16065  telgsums  17217  psrbaglefi  18218  psrbaglefiOLD  18219  gsummoncoe1  18541  psgndiflemA  18810  isphld  18862  gsummatr01lem3  19326  cpmatmcllem  19386  mp2pm2mplem4  19477  chfacfisf  19522  chfacfisfcpmat  19523  cayleyhamilton1  19560  tgcl  19638  neindisj2  19791  2ndcdisj  20123  fgcl  20545  rnelfm  20620  alexsubALTlem3  20715  usgraexmpledg  24605  usgrares1  24612  usgrafis  24617  nbgraf1olem5  24647  nbcusgra  24665  cusgrares  24674  cusgrasize  24680  usgrnloop  24767  pthdepisspth  24778  usgra2adedgspthlem2  24814  usgra2wlkspth  24823  fargshiftfva  24841  usgrcyclnl2  24843  wwlkextinj  24932  wwlkextproplem2  24944  clwlkisclwwlklem2a  24987  clwlkisclwwlklem1  24989  clwwlkf1  24998  clwlkfclwwlk  25046  el2spthonot  25072  2spontn0vne  25089  eupatrl  25170  frgra3vlem1  25202  3vfriswmgralem  25206  vdgn0frgrav2  25226  vdgn1frgrav2  25228  frgrancvvdeqlemC  25241  frgrancvvdgeq  25245  frgrawopreglem5  25250  frg2woteq  25262  usg2spot2nb  25267  2spotmdisj  25270  extwwlkfablem2  25280  numclwwlkovf2ex  25288  rngoueqz  25630  mdexchi  27452  atomli  27499  mdsymlem5  27524  sumdmdlem  27535  dfimafnf  27694  mclsind  29194  dfon2lem6  29460  predpo  29504  btwnconn1lem11  29975  itg2addnc  30309  finminlem  30376  dmncan1  30713  eldioph2  30934  funressnfv  32452  dfaimafn  32489  otiunsndisjX  32675  elfz2z  32705  usgra2pthlem1  32725  zrtermorngc  33063  zrtermoringc  33132  snlindsntor  33326  ldepspr  33328  nn0sumshdiglemB  33495  bnj517  34344  bnj1118  34441  lshpdisj  35109  2at0mat0  35646  llncvrlpln2  35678  lplncvrlvol2  35736  lhpexle2lem  36130  cdlemk33N  37032  cdlemk34  37033
  Copyright terms: Public domain W3C validator