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

Theorem imp31 432
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 429 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  ->  th )
)
32imp 429 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 371
This theorem is referenced by:  imp41  593  imp5d  599  impl  620  anassrs  648  an31s  804  3imp  1181  3expa  1187  reusv3  4512  pwssun  4639  fri  4694  ordelord  4753  tz7.7  4757  dfimafn  5752  funimass4  5754  funimass3  5831  isomin  6040  isopolem  6048  onint  6418  limsssuc  6473  tfindsg  6483  findsg  6515  suppfnss  6726  smores2  6827  tfrlem9  6856  tz7.49  6912  oecl  6989  oaordi  6997  oaass  7012  omordi  7017  odi  7030  oen0  7037  nnaordi  7069  nnmordi  7082  php3  7509  domunfican  7596  dfac5  8310  cofsmo  8450  cfcoflem  8453  zorn2lem7  8683  tskwun  8963  mulcanpi  9081  ltexprlem7  9223  sup3  10299  elnnz  10668  uzletr  10881  irradd  10989  irrmul  10990  uzsubsubfz  11483  elfzonelfzo  11639  uzindi  11815  sqlecan  11984  swrdnd  12338  wrd2ind  12384  cshwlen  12448  cshwidxmod  12452  unbenlem  13981  infpnlem1  13983  iscatd  14623  dirtr  15418  psrbaglefi  17453  psrbaglefiOLD  17454  psgndiflemA  18043  isphld  18095  tgcl  18586  neindisj2  18739  bwthOLD  19026  2ndcdisj  19072  fgcl  19463  rnelfm  19538  alexsubALTlem3  19633  usgrares1  23335  usgrafis  23340  nbgraf1olem5  23366  nbcusgra  23383  cusgrares  23392  cusgrasize  23398  usgrnloop  23474  pthdepisspth  23485  fargshiftfva  23537  usgrcyclnl2  23539  eupatrl  23601  rngoueqz  23929  mdexchi  25751  atomli  25798  mdsymlem5  25823  sumdmdlem  25834  dfimafnf  25962  dfon2lem6  27613  predpo  27657  btwnconn1lem11  28140  itg2addnc  28458  finminlem  28525  dmncan1  28888  eldioph2  29112  funressnfv  30046  dfaimafn  30083  otiunsndisj  30144  otiunsndisjX  30145  uzuzle  30202  elfz2z  30210  usgra2wlkspth  30310  usgra2pthlem1  30312  usgra2adedgspthlem2  30316  el2spthonot  30401  2spontn0vne  30418  clwlkisclwwlklem2a  30459  clwwlkf1  30470  cshwlemma1  30501  clwlkfclwwlk  30529  wwlkextproplem2  30573  frgra3vlem1  30604  3vfriswmgralem  30608  vdgn0frgrav2  30629  vdgn1frgrav2  30631  frgrancvvdeqlemC  30644  frgrancvvdgeq  30648  frgrawopreglem5  30653  frg2woteq  30665  usg2spot2nb  30670  2spotmdisj  30673  extwwlkfablem2  30683  numclwwlkovf2ex  30691  ssnn0fi  30758  telescgsum  30823  gsummoncoe1  30855  scmatmulcl  30898  mp2pm2mplem4  30931  snlindsntor  31017  ldepspr  31019  bnj517  31890  bnj1118  31987  lshpdisj  32644  2at0mat0  33181  llncvrlpln2  33213  lplncvrlvol2  33271  lhpexle2lem  33665  cdlemk33N  34565  cdlemk34  34566
  Copyright terms: Public domain W3C validator