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  1189  3expa  1195  reusv3  4641  otiunsndisj  4739  pwssun  4772  fri  4827  ordelord  4886  tz7.7  4890  dfimafn  5903  funimass4  5905  funimass3  5984  isomin  6214  isopolem  6222  onint  6611  limsssuc  6666  tfindsg  6676  findsg  6708  suppfnss  6923  smores2  7023  tfrlem9  7052  tz7.49  7108  oecl  7185  oaordi  7193  oaass  7208  omordi  7213  odi  7226  oen0  7233  nnaordi  7265  nnmordi  7278  php3  7701  domunfican  7791  dfac5  8507  cofsmo  8647  cfcoflem  8650  zorn2lem7  8880  tskwun  9160  mulcanpi  9276  ltexprlem7  9418  sup3  10501  elnnz  10875  irradd  11210  irrmul  11211  uzsubsubfz  11711  fzo1fzo0n0  11838  elfzonelfzo  11886  uzindi  12065  ssnn0fi  12068  sqlecan  12248  swrdnd  12631  wrd2ind  12677  repswccat  12731  cshwlen  12744  cshwidxmod  12748  2cshwcshw  12767  unbenlem  14298  infpnlem1  14300  iscatd  14942  dirtr  15735  telgsums  16891  psrbaglefi  17891  psrbaglefiOLD  17892  gsummoncoe1  18214  psgndiflemA  18504  isphld  18556  gsummatr01lem3  19026  cpmatmcllem  19086  mp2pm2mplem4  19177  chfacfisf  19222  chfacfisfcpmat  19223  cayleyhamilton1  19260  tgcl  19337  neindisj2  19490  bwthOLD  19777  2ndcdisj  19823  fgcl  20245  rnelfm  20320  alexsubALTlem3  20415  usgraexmpledg  24268  usgrares1  24275  usgrafis  24280  nbgraf1olem5  24310  nbcusgra  24328  cusgrares  24337  cusgrasize  24343  usgrnloop  24430  pthdepisspth  24441  usgra2adedgspthlem2  24477  usgra2wlkspth  24486  fargshiftfva  24504  usgrcyclnl2  24506  wwlkextinj  24595  wwlkextproplem2  24607  clwlkisclwwlklem2a  24650  clwlkisclwwlklem1  24652  clwwlkf1  24661  clwlkfclwwlk  24709  el2spthonot  24735  2spontn0vne  24752  eupatrl  24833  frgra3vlem1  24865  3vfriswmgralem  24869  vdgn0frgrav2  24889  vdgn1frgrav2  24891  frgrancvvdeqlemC  24904  frgrancvvdgeq  24908  frgrawopreglem5  24913  frg2woteq  24925  usg2spot2nb  24930  2spotmdisj  24933  extwwlkfablem2  24943  numclwwlkovf2ex  24951  rngoueqz  25297  mdexchi  27119  atomli  27166  mdsymlem5  27191  sumdmdlem  27202  dfimafnf  27338  mclsind  28796  dfon2lem6  29188  predpo  29232  btwnconn1lem11  29715  itg2addnc  30037  finminlem  30104  dmncan1  30441  eldioph2  30663  funressnfv  32047  dfaimafn  32084  otiunsndisjX  32135  elfz2z  32165  usgra2pthlem1  32187  snlindsntor  32782  ldepspr  32784  bnj517  33650  bnj1118  33747  lshpdisj  34414  2at0mat0  34951  llncvrlpln2  34983  lplncvrlvol2  35041  lhpexle2lem  35435  cdlemk33N  36337  cdlemk34  36338
  Copyright terms: Public domain W3C validator