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

Theorem 3impib 1189
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 1185 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 970
This theorem is referenced by:  mob  3278  eqreu  3288  dedth3h  3986  ssimaexg  5924  dfsmo2  7008  omwordri  7211  3ecoptocl  7393  cfslb  8635  cofsmo  8638  cfsmolem  8639  coftr  8642  domtriomlem  8811  zorn2lem7  8871  ttukey2g  8885  gchi  8991  tskxpss  9139  tskord  9147  infm3  10491  uzind  10941  fzind  10948  fnn0ind  10949  xltnegi  11404  axdc4uz  12049  facwordi  12322  lswccatn0lsw  12558  swrdvalodm2  12614  swrdvalodm  12615  cshwidxmod  12724  caubnd  13140  mulgcd  14032  pcfac  14266  ramz  14391  imasleval  14785  drsdir  15411  psasym  15686  pstr  15687  tsrlin  15695  dirge  15713  mhmlin  15777  mhmmulg  15967  issubg2  16004  nsgbi  16020  cygabl  16677  gsumcom2  16787  srgmulgass  16963  dvdsrtr  17078  drnginvrcl  17189  drnginvrn0  17190  drnginvrl  17191  drnginvrr  17192  isdrngd  17197  issubrg2  17225  abvmul  17254  abvtri  17255  lmhmlin  17457  domnmuln0  17711  ipcj  18429  cssincl  18479  obsip  18512  decpmatmulsumfsupp  19034  mp2pm2mplem4  19070  pm2mpghm  19077  pm2mpmhmlem1  19079  inopn  19168  basis1  19211  iscldtop  19355  2ndcdisj  19716  cnmpt2t  19902  cnmpt22  19903  cnmptcom  19907  fbasssin  20065  ptcmplem3  20282  xmeteq0  20569  prdsxmslem2  20760  metustsym  20793  nmvs  20913  nmolb  20952  volfiniun  21685  sincosq1sgn  22617  sincosq2sgn  22618  sincosq3sgn  22619  sincosq4sgn  22620  usg2wlk  24279  wwlknext  24386  wwlkext2clwwlk  24465  cusgraisrusgra  24600  rusgra0edg  24617  numclwwlkovf2ex  24749  ablocom  24949  nmcvcn  25267  ipassi  25418  htth  25497  shaddcl  25796  shmulcl  25797  shsubcl  25800  chlimi  25814  pjspansn  26157  cnopc  26494  cnfnc  26511  adj1  26514  lnfnmul  26629  atord  26969  atcvat2  26970  cdj3i  27022  nexple  27631  pconcn  28295  shftvalg  28577  wfr3g  28905  frr3g  28949  linethru  29366  sin2h  29609  cos2h  29610  tan2h  29611  dvasin  29667  areacirclem1  29671  ismrc  30224  fzsplit1nn0  30278  pell1234qrmulcl  30382  pell14qrmulcl  30390  stoweidlem17  31272  zm1nn  31749  mgmcl  31848  ztprmneprm  31875  lcoel0  31977  linindslinci  31997  bi23impib  32208  bi13impib  32209  trelded  32293  suctrALT  32581  suctrALTcf  32677  suctrALTcfVD  32678  bnj910  32960  bnj1154  33009  riotasv  33637  lsmsatcv  33682  omllaw  33915  2llnjN  34238  dalawlem10  34551  dalawlem13  34554  dalawlem14  34555  pclfinclN  34621
  Copyright terms: Public domain W3C validator