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

Theorem 3impib 1206
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impib.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
3impib  |-  ( (
ph  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3impib
StepHypRef Expression
1 3impib.1 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21expd 438 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1202 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  mob  3220  eqreu  3230  dedth3h  3934  ssimaexg  5931  wfr3g  7034  dfsmo2  7066  omwordri  7273  3ecoptocl  7455  cfslb  8696  cofsmo  8699  cfsmolem  8700  coftr  8703  domtriomlem  8872  zorn2lem7  8932  ttukey2g  8946  gchi  9049  tskxpss  9197  tskord  9205  infm3  10568  uzind  11027  fzind  11033  fnn0ind  11034  xltnegi  11509  axdc4uz  12196  facwordi  12474  swrdnd2  12789  cshwidxmod  12905  relexpsucr  13092  relexpsucl  13096  relexprelg  13101  relexpaddnn  13114  caubnd  13421  mulgcd  14514  lcmfdvds  14615  lcmfdvdsb  14616  pcfac  14844  ramz  14983  imasleval  15447  cictr  15710  initoeu2lem1  15909  drsdir  16180  psasym  16456  pstr  16457  tsrlin  16465  dirge  16483  mgmcl  16491  mhmlin  16589  mhmmulg  16790  issubg2  16832  nsgbi  16848  cygabl  17525  gsumcom2  17607  srgmulgass  17764  dvdsrtr  17880  drnginvrcl  17992  drnginvrn0  17993  drnginvrl  17994  drnginvrr  17995  isdrngd  18000  issubrg2  18028  abvmul  18057  abvtri  18058  lmhmlin  18258  domnmuln0  18522  ipcj  19201  cssincl  19251  obsip  19284  decpmatmulsumfsupp  19797  mp2pm2mplem4  19833  pm2mpghm  19840  pm2mpmhmlem1  19842  inopn  19929  basis1  19965  iscldtop  20111  2ndcdisj  20471  cnmpt2t  20688  cnmpt22  20689  cnmptcom  20693  fbasssin  20851  ptcmplem3  21069  xmeteq0  21353  prdsxmslem2  21544  nmvs  21679  nmolb  21722  nmolbOLD  21741  volfiniun  22500  sincosq1sgn  23453  sincosq2sgn  23454  sincosq3sgn  23455  sincosq4sgn  23456  usg2wlk  25345  wwlknext  25452  wwlkext2clwwlk  25531  cusgraisrusgra  25666  rusgra0edg  25683  numclwwlkovf2ex  25814  ablocom  26013  nmcvcn  26331  ipassi  26482  htth  26571  shaddcl  26870  shmulcl  26871  shsubcl  26873  chlimi  26887  pjspansn  27230  cnopc  27566  cnfnc  27583  adj1  27586  lnfnmul  27701  atord  28041  atcvat2  28042  cdj3i  28094  nexple  28831  signstfvc  29463  bnj910  29759  bnj1154  29808  pconcn  29947  mrsubccat  30156  shftvalg  30365  frr3g  30513  linethru  30920  sin2h  31935  cos2h  31936  tan2h  31937  dvasin  32028  areacirclem1  32032  riotasv  32531  lsmsatcv  32576  omllaw  32809  2llnjN  33132  dalawlem10  33445  dalawlem13  33448  dalawlem14  33449  pclfinclN  33515  ismrc  35543  fzsplit1nn0  35596  pell1234qrmulcl  35701  pell14qrmulcl  35709  iunrelexp0  36294  bi23impib  36841  bi13impib  36842  trelded  36932  suctrALT  37222  suctrALTcf  37319  suctrALTcfVD  37320  stoweidlem17  37877  bgoldbtbndlem4  38903  bgoldbtbnd  38904  tgblthelfgott  38908  zm1nn  39049  ewlkle  39623  mgmhmlin  39839  issubmgm2  39843  clcllaw  39880  rnghmmul  39953  ztprmneprm  40181  lcoel0  40274  linindslinci  40294
  Copyright terms: Public domain W3C validator