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

Theorem imp32 424
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 422 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32imp 420 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  imp42  579  impr  604  anasss  630  an13s  780  3expb  1155  reuss2  3623  reupick  3627  po2nr  4519  tz7.7  4610  ordtr2  4628  onint  4778  fvmptt  5823  fliftfund  6038  isomin  6060  f1ocnv2d  6298  tfrlem5  6644  tz7.48lem  6701  oalimcl  6806  oaass  6807  omass  6826  omabs  6893  finsschain  7416  infxpenlem  7900  axcc3  8323  zorn2lem7  8387  addclpi  8774  addnidpi  8783  genpnnp  8887  genpnmax  8889  mulclprlem  8901  prodgt0  9860  ltsubrp  10648  ltaddrp  10649  infpnlem1  13283  iscatd  13903  joinle  14455  imasmnd2  14737  imasgrp2  14938  imasrng  15730  0ntr  17140  clsndisj  17144  innei  17194  islpi  17218  tgcnp  17322  haust1  17421  alexsublem  18080  alexsubb  18082  isxmetd  18361  grpoidinvlem3  21799  elspansn5  23081  5oalem6  23166  mdi  23803  dmdi  23810  dmdsl3  23823  atom1d  23861  cvexchlem  23876  atcvatlem  23893  chirredlem3  23900  mdsymlem5  23915  f1o3d  24046  dedekindle  25193  dfon2lem6  25420  frmin  25522  soseq  25534  nodenselem5  25645  nodense  25649  axcontlem4  25911  broutsideof2  26061  outsideoftr  26068  outsideofeq  26069  nndivsub  26212  bddiblnc  26289  ftc1anc  26302  elicc3  26334  nn0prpwlem  26339  cntotbnd  26519  heiborlem6  26539  pridlc3  26697  swrdccatin1  28239  swrdccat3  28249  wwlknimp  28369  bnj570  29350  leat2  30166  cvrexchlem  30290  cvratlem  30292  3dim2  30339  ps-2  30349  lncvrelatN  30652  osumcllem11N  30837
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 179  df-an 362
  Copyright terms: Public domain W3C validator