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

Theorem 3impib 1195
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 436 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1191 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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  df-3an 976
This theorem is referenced by:  mob  3267  eqreu  3277  dedth3h  3980  ssimaexg  5924  dfsmo2  7020  omwordri  7223  3ecoptocl  7405  cfslb  8649  cofsmo  8652  cfsmolem  8653  coftr  8656  domtriomlem  8825  zorn2lem7  8885  ttukey2g  8899  gchi  9005  tskxpss  9153  tskord  9161  infm3  10509  uzind  10961  fzind  10968  fnn0ind  10969  xltnegi  11425  axdc4uz  12074  facwordi  12348  lswccatn0lsw  12588  swrdvalodm2  12645  swrdvalodm  12646  cshwidxmod  12755  caubnd  13172  mulgcd  14165  pcfac  14399  ramz  14524  imasleval  14919  drsdir  15542  psasym  15818  pstr  15819  tsrlin  15827  dirge  15845  mgmcl  15853  mhmlin  15951  mhmmulg  16152  issubg2  16194  nsgbi  16210  cygabl  16871  gsumcom2  16981  srgmulgass  17160  dvdsrtr  17279  drnginvrcl  17391  drnginvrn0  17392  drnginvrl  17393  drnginvrr  17394  isdrngd  17399  issubrg2  17427  abvmul  17456  abvtri  17457  lmhmlin  17659  domnmuln0  17925  ipcj  18646  cssincl  18696  obsip  18729  decpmatmulsumfsupp  19251  mp2pm2mplem4  19287  pm2mpghm  19294  pm2mpmhmlem1  19296  inopn  19385  basis1  19428  iscldtop  19573  2ndcdisj  19934  cnmpt2t  20151  cnmpt22  20152  cnmptcom  20156  fbasssin  20314  ptcmplem3  20531  xmeteq0  20818  prdsxmslem2  21009  nmvs  21162  nmolb  21201  volfiniun  21934  sincosq1sgn  22867  sincosq2sgn  22868  sincosq3sgn  22869  sincosq4sgn  22870  usg2wlk  24593  wwlknext  24700  wwlkext2clwwlk  24779  cusgraisrusgra  24914  rusgra0edg  24931  numclwwlkovf2ex  25062  ablocom  25263  nmcvcn  25581  ipassi  25732  htth  25811  shaddcl  26110  shmulcl  26111  shsubcl  26114  chlimi  26128  pjspansn  26471  cnopc  26808  cnfnc  26825  adj1  26828  lnfnmul  26943  atord  27283  atcvat2  27284  cdj3i  27336  nexple  27982  signstfvc  28508  pconcn  28646  mrsubccat  28855  shftvalg  29092  wfr3g  29317  frr3g  29361  linethru  29778  sin2h  30020  cos2h  30021  tan2h  30022  dvasin  30078  areacirclem1  30082  ismrc  30608  fzsplit1nn0  30662  pell1234qrmulcl  30766  pell14qrmulcl  30774  stoweidlem17  31688  zm1nn  32163  mgmhmlin  32312  issubmgm2  32316  clcllaw  32352  rnghmmul  32424  ztprmneprm  32669  lcoel0  32764  linindslinci  32784  bi23impib  32987  bi13impib  32988  trelded  33071  suctrALT  33359  suctrALTcf  33455  suctrALTcfVD  33456  bnj910  33739  bnj1154  33788  riotasv  34430  lsmsatcv  34475  omllaw  34708  2llnjN  35031  dalawlem10  35344  dalawlem13  35347  dalawlem14  35348  pclfinclN  35414
  Copyright terms: Public domain W3C validator