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

Theorem imp32 423
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp3.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Assertion
Ref Expression
imp32  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )

Proof of Theorem imp32
StepHypRef Expression
1 imp3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21imp3a 421 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32imp 419 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  imp42  578  impr  603  anasss  629  an13s  779  3expb  1154  reuss2  3613  reupick  3617  po2nr  4508  tz7.7  4599  ordtr2  4617  onint  4767  fvmptt  5812  fliftfund  6027  isomin  6049  f1ocnv2d  6287  tfrlem5  6633  tz7.48lem  6690  oalimcl  6795  oaass  6796  omass  6815  omabs  6882  finsschain  7405  infxpenlem  7887  axcc3  8310  zorn2lem7  8374  addclpi  8761  addnidpi  8770  genpnnp  8874  genpnmax  8876  mulclprlem  8888  prodgt0  9847  ltsubrp  10635  ltaddrp  10636  infpnlem1  13270  iscatd  13890  joinle  14442  imasmnd2  14724  imasgrp2  14925  imasrng  15717  0ntr  17127  clsndisj  17131  innei  17181  islpi  17205  tgcnp  17309  haust1  17408  alexsublem  18067  alexsubb  18069  isxmetd  18348  grpoidinvlem3  21786  elspansn5  23068  5oalem6  23153  mdi  23790  dmdi  23797  dmdsl3  23810  atom1d  23848  cvexchlem  23863  atcvatlem  23880  chirredlem3  23887  mdsymlem5  23902  f1o3d  24033  dedekindle  25180  dfon2lem6  25407  frmin  25509  soseq  25521  nodenselem5  25632  nodense  25636  axcontlem4  25898  broutsideof2  26048  outsideoftr  26055  outsideofeq  26056  nndivsub  26199  bddiblnc  26265  ftc1anc  26278  elicc3  26311  nn0prpwlem  26316  cntotbnd  26496  heiborlem6  26516  pridlc3  26674  swrdccatin1  28171  swrdccat3  28181  bnj570  29213  leat2  30029  cvrexchlem  30153  cvratlem  30155  3dim2  30202  ps-2  30212  lncvrelatN  30515  osumcllem11N  30700
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 178  df-an 361
  Copyright terms: Public domain W3C validator