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

Theorem 3impib 1203
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 437 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1199 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  mob  3253  eqreu  3263  dedth3h  3962  ssimaexg  5944  wfr3g  7039  dfsmo2  7071  omwordri  7278  3ecoptocl  7460  cfslb  8697  cofsmo  8700  cfsmolem  8701  coftr  8704  domtriomlem  8873  zorn2lem7  8933  ttukey2g  8947  gchi  9050  tskxpss  9198  tskord  9206  infm3  10569  uzind  11028  fzind  11034  fnn0ind  11035  xltnegi  11510  axdc4uz  12196  facwordi  12474  swrdnd2  12780  cshwidxmod  12896  relexpsucr  13081  relexpsucl  13085  relexprelg  13090  relexpaddnn  13103  caubnd  13410  mulgcd  14502  lcmfdvds  14603  lcmfdvdsb  14604  pcfac  14832  ramz  14971  imasleval  15435  cictr  15698  initoeu2lem1  15897  drsdir  16168  psasym  16444  pstr  16445  tsrlin  16453  dirge  16471  mgmcl  16479  mhmlin  16577  mhmmulg  16778  issubg2  16820  nsgbi  16836  cygabl  17513  gsumcom2  17595  srgmulgass  17752  dvdsrtr  17868  drnginvrcl  17980  drnginvrn0  17981  drnginvrl  17982  drnginvrr  17983  isdrngd  17988  issubrg2  18016  abvmul  18045  abvtri  18046  lmhmlin  18246  domnmuln0  18510  ipcj  19188  cssincl  19238  obsip  19271  decpmatmulsumfsupp  19784  mp2pm2mplem4  19820  pm2mpghm  19827  pm2mpmhmlem1  19829  inopn  19916  basis1  19952  iscldtop  20098  2ndcdisj  20458  cnmpt2t  20675  cnmpt22  20676  cnmptcom  20680  fbasssin  20838  ptcmplem3  21056  xmeteq0  21340  prdsxmslem2  21531  nmvs  21666  nmolb  21709  nmolbOLD  21728  volfiniun  22487  sincosq1sgn  23440  sincosq2sgn  23441  sincosq3sgn  23442  sincosq4sgn  23443  usg2wlk  25331  wwlknext  25438  wwlkext2clwwlk  25517  cusgraisrusgra  25652  rusgra0edg  25669  numclwwlkovf2ex  25800  ablocom  25999  nmcvcn  26317  ipassi  26468  htth  26557  shaddcl  26856  shmulcl  26857  shsubcl  26859  chlimi  26873  pjspansn  27216  cnopc  27552  cnfnc  27569  adj1  27572  lnfnmul  27687  atord  28027  atcvat2  28028  cdj3i  28080  nexple  28827  signstfvc  29459  bnj910  29755  bnj1154  29804  pconcn  29943  mrsubccat  30152  shftvalg  30360  frr3g  30508  linethru  30913  sin2h  31849  cos2h  31850  tan2h  31851  dvasin  31942  areacirclem1  31946  riotasv  32450  lsmsatcv  32495  omllaw  32728  2llnjN  33051  dalawlem10  33364  dalawlem13  33367  dalawlem14  33368  pclfinclN  33434  ismrc  35462  fzsplit1nn0  35515  pell1234qrmulcl  35621  pell14qrmulcl  35629  iunrelexp0  36154  bi23impib  36699  bi13impib  36700  trelded  36790  suctrALT  37083  suctrALTcf  37180  suctrALTcfVD  37181  stoweidlem17  37697  bgoldbtbndlem4  38615  bgoldbtbnd  38616  tgblthelfgott  38620  zm1nn  38738  mgmhmlin  39058  issubmgm2  39062  clcllaw  39099  rnghmmul  39172  ztprmneprm  39402  lcoel0  39495  linindslinci  39515
  Copyright terms: Public domain W3C validator