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  2960  eqreu  2970  dedth3h  3621  ssimaexg  5601  riotasv  6368  dfsmo2  6380  omwordri  6586  3ecoptocl  6766  cfslb  7908  cofsmo  7911  cfsmolem  7912  coftr  7915  domtriomlem  8084  zorn2lem7  8145  ttukey2g  8159  gchi  8262  tskxpss  8410  tskord  8418  infm3  9729  uzind  10119  fzind  10126  fnn0ind  10127  xltnegi  10559  axdc4uz  11061  facwordi  11318  caubnd  11858  mulgcd  12741  pcfac  12963  ramz  13088  imasleval  13459  drsdir  14085  latlem  14170  psasym  14335  pstr  14336  tsrlin  14344  dirge  14375  mhmlin  14438  mhmmulg  14615  issubg2  14652  nsgbi  14664  cygabl  15193  gsumcom2  15242  dvdsrtr  15450  drnginvrcl  15545  drnginvrn0  15546  drnginvrl  15547  drnginvrr  15548  isdrngd  15553  issubrg2  15581  abvmul  15610  abvtri  15611  lmhmlin  15808  domnmuln0  16055  ipcj  16554  cssincl  16604  obsip  16637  inopn  16661  basis1  16704  iscldtop  16848  2ndcdisj  17198  cnmpt2t  17383  cnmpt22  17384  cnmptcom  17388  fbasssin  17547  ptcmplem3  17764  xmeteq0  17919  prdsxmslem2  18091  nmvs  18203  nmolb  18242  volfiniun  18920  sincosq1sgn  19882  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  ablocom  20968  nmcvcn  21284  ipassi  21435  htth  21514  shaddcl  21812  shmulcl  21813  shsubcl  21816  chlimi  21830  pjspansn  22172  cnopc  22509  cnfnc  22526  adj1  22529  lnfnmul  22644  atord  22984  atcvat2  22985  cdj3i  23037  abfmpeld  23233  pconcn  23770  wfr3g  24326  frr3g  24351  linethru  24848  dvreasin  25026  areacirclem2  25028  oooeqim2  25156  cmppfd  25848  domcmpd  25849  codcmpd  25850  cmpida  25877  cmpidb  25878  ishomd  25893  ismrc  26879  fzsplit1nn0  26936  pell1234qrmulcl  27043  pell14qrmulcl  27051  stoweidlem17  27869  bi23impib  28549  bi13impib  28550  bi123impib  28551  trelded  28630  suctrALTcf  29014  suctrALTcfVD  29015  suctrALT4  29020  bnj910  29296  bnj1154  29345  a12study4  29739  lsmsatcv  29822  omllaw  30055  2llnjN  30378  dalawlem10  30691  dalawlem13  30694  dalawlem14  30695  pclfinclN  30761
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