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

Theorem 3impib 1180
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 )
)
21exp3a 436 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1176 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 960
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 962
This theorem is referenced by:  mob  3138  eqreu  3148  dedth3h  3840  ssimaexg  5754  dfsmo2  6804  omwordri  7007  3ecoptocl  7188  cfslb  8431  cofsmo  8434  cfsmolem  8435  coftr  8438  domtriomlem  8607  zorn2lem7  8667  ttukey2g  8681  gchi  8787  tskxpss  8935  tskord  8943  infm3  10285  uzind  10729  fzind  10736  fnn0ind  10737  xltnegi  11182  axdc4uz  11801  facwordi  12061  lswccatn0lsw  12283  swrdvalodm2  12329  swrdvalodm  12330  cshwidxmod  12436  caubnd  12842  mulgcd  13726  pcfac  13957  ramz  14082  imasleval  14475  drsdir  15101  psasym  15376  pstr  15377  tsrlin  15385  dirge  15403  mhmlin  15467  mhmmulg  15652  issubg2  15689  nsgbi  15705  cygabl  16360  gsumcom2  16457  srgmulgass  16620  dvdsrtr  16734  drnginvrcl  16829  drnginvrn0  16830  drnginvrl  16831  drnginvrr  16832  isdrngd  16837  issubrg2  16865  abvmul  16894  abvtri  16895  lmhmlin  17094  domnmuln0  17348  ipcj  18022  cssincl  18072  obsip  18105  inopn  18471  basis1  18514  iscldtop  18658  2ndcdisj  19019  cnmpt2t  19205  cnmpt22  19206  cnmptcom  19210  fbasssin  19368  ptcmplem3  19585  xmeteq0  19872  prdsxmslem2  20063  metustsym  20096  nmvs  20216  nmolb  20255  volfiniun  20987  sincosq1sgn  21919  sincosq2sgn  21920  sincosq3sgn  21921  sincosq4sgn  21922  ablocom  23707  nmcvcn  24025  ipassi  24176  htth  24255  shaddcl  24554  shmulcl  24555  shsubcl  24558  chlimi  24572  pjspansn  24915  cnopc  25252  cnfnc  25269  adj1  25272  lnfnmul  25387  atord  25727  atcvat2  25728  cdj3i  25780  nexple  26384  pconcn  27043  shftvalg  27324  wfr3g  27652  frr3g  27696  linethru  28113  sin2h  28347  cos2h  28348  tan2h  28349  dvasin  28405  areacirclem1  28409  ismrc  28962  fzsplit1nn0  29017  pell1234qrmulcl  29121  pell14qrmulcl  29129  stoweidlem17  29737  usg2wlk  30234  wwlknext  30281  wwlkext2clwwlk  30390  zm1nn  30393  cusgraisrusgra  30476  rusgra0edg  30498  numclwwlkovf2ex  30604  ztprmneprm  30663  lcoel0  30803  linindslinci  30823  bi23impib  31022  bi13impib  31023  trelded  31107  suctrALT  31396  suctrALTcf  31492  suctrALTcfVD  31493  bnj910  31775  bnj1154  31824  riotasv  32332  lsmsatcv  32377  omllaw  32610  2llnjN  32933  dalawlem10  33246  dalawlem13  33249  dalawlem14  33250  pclfinclN  33316
  Copyright terms: Public domain W3C validator