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

Theorem 3impib 1149
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 425 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1145 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  mob  2947  eqreu  2957  dedth3h  3608  ssimaexg  5585  riotasv  6352  dfsmo2  6364  omwordri  6570  3ecoptocl  6750  cfslb  7892  cofsmo  7895  cfsmolem  7896  coftr  7899  domtriomlem  8068  zorn2lem7  8129  ttukey2g  8143  gchi  8246  tskxpss  8394  tskord  8402  infm3  9713  uzind  10103  fzind  10110  fnn0ind  10111  xltnegi  10543  axdc4uz  11045  facwordi  11302  caubnd  11842  mulgcd  12725  pcfac  12947  ramz  13072  imasleval  13443  drsdir  14069  latlem  14154  psasym  14319  pstr  14320  tsrlin  14328  dirge  14359  mhmlin  14422  mhmmulg  14599  issubg2  14636  nsgbi  14648  cygabl  15177  gsumcom2  15226  dvdsrtr  15434  drnginvrcl  15529  drnginvrn0  15530  drnginvrl  15531  drnginvrr  15532  isdrngd  15537  issubrg2  15565  abvmul  15594  abvtri  15595  lmhmlin  15792  domnmuln0  16039  ipcj  16538  cssincl  16588  obsip  16621  inopn  16645  basis1  16688  iscldtop  16832  2ndcdisj  17182  cnmpt2t  17367  cnmpt22  17368  cnmptcom  17372  fbasssin  17531  ptcmplem3  17748  xmeteq0  17903  prdsxmslem2  18075  nmvs  18187  nmolb  18226  volfiniun  18904  sincosq1sgn  19866  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  ablocom  20952  nmcvcn  21268  ipassi  21419  htth  21498  shaddcl  21796  shmulcl  21797  shsubcl  21800  chlimi  21814  pjspansn  22156  cnopc  22493  cnfnc  22510  adj1  22513  lnfnmul  22628  atord  22968  atcvat2  22969  cdj3i  23021  abfmpeld  23218  pconcn  23755  wfr3g  24255  frr3g  24280  linethru  24776  dvreasin  24923  areacirclem2  24925  oooeqim2  25053  cmppfd  25745  domcmpd  25746  codcmpd  25747  cmpida  25774  cmpidb  25775  ishomd  25790  ismrc  26776  fzsplit1nn0  26833  pell1234qrmulcl  26940  pell14qrmulcl  26948  stoweidlem17  27766  trelded  28331  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT4  28704  bnj910  28980  bnj1154  29029  a12study4  29117  lsmsatcv  29200  omllaw  29433  2llnjN  29756  dalawlem10  30069  dalawlem13  30072  dalawlem14  30073  pclfinclN  30139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator