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

Theorem 3impib 1185
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 1181 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  mob  3144  eqreu  3154  dedth3h  3846  ssimaexg  5760  dfsmo2  6811  omwordri  7014  3ecoptocl  7195  cfslb  8438  cofsmo  8441  cfsmolem  8442  coftr  8445  domtriomlem  8614  zorn2lem7  8674  ttukey2g  8688  gchi  8794  tskxpss  8942  tskord  8950  infm3  10292  uzind  10736  fzind  10743  fnn0ind  10744  xltnegi  11189  axdc4uz  11808  facwordi  12068  lswccatn0lsw  12290  swrdvalodm2  12336  swrdvalodm  12337  cshwidxmod  12443  caubnd  12849  mulgcd  13733  pcfac  13964  ramz  14089  imasleval  14482  drsdir  15108  psasym  15383  pstr  15384  tsrlin  15392  dirge  15410  mhmlin  15474  mhmmulg  15662  issubg2  15699  nsgbi  15715  cygabl  16370  gsumcom2  16470  srgmulgass  16633  dvdsrtr  16747  drnginvrcl  16852  drnginvrn0  16853  drnginvrl  16854  drnginvrr  16855  isdrngd  16860  issubrg2  16888  abvmul  16917  abvtri  16918  lmhmlin  17119  domnmuln0  17373  ipcj  18066  cssincl  18116  obsip  18149  inopn  18515  basis1  18558  iscldtop  18702  2ndcdisj  19063  cnmpt2t  19249  cnmpt22  19250  cnmptcom  19254  fbasssin  19412  ptcmplem3  19629  xmeteq0  19916  prdsxmslem2  20107  metustsym  20140  nmvs  20260  nmolb  20299  volfiniun  21031  sincosq1sgn  21963  sincosq2sgn  21964  sincosq3sgn  21965  sincosq4sgn  21966  ablocom  23775  nmcvcn  24093  ipassi  24244  htth  24323  shaddcl  24622  shmulcl  24623  shsubcl  24626  chlimi  24640  pjspansn  24983  cnopc  25320  cnfnc  25337  adj1  25340  lnfnmul  25455  atord  25795  atcvat2  25796  cdj3i  25848  nexple  26451  pconcn  27116  shftvalg  27398  wfr3g  27726  frr3g  27770  linethru  28187  sin2h  28425  cos2h  28426  tan2h  28427  dvasin  28483  areacirclem1  28487  ismrc  29040  fzsplit1nn0  29095  pell1234qrmulcl  29199  pell14qrmulcl  29207  stoweidlem17  29815  usg2wlk  30312  wwlknext  30359  wwlkext2clwwlk  30468  zm1nn  30471  cusgraisrusgra  30554  rusgra0edg  30576  numclwwlkovf2ex  30682  ztprmneprm  30742  mp2pm2mplem4  30922  pmattomply1ghm  30928  pmattomply1mhmlem0  30930  pmattomply1mhmlem1  30931  lcoel0  30965  linindslinci  30985  bi23impib  31192  bi13impib  31193  trelded  31277  suctrALT  31565  suctrALTcf  31661  suctrALTcfVD  31662  bnj910  31944  bnj1154  31993  riotasv  32613  lsmsatcv  32658  omllaw  32891  2llnjN  33214  dalawlem10  33527  dalawlem13  33530  dalawlem14  33531  pclfinclN  33597
  Copyright terms: Public domain W3C validator