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

Theorem 3impib 1152
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 427 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1148 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  mob  3117  eqreu  3127  dedth3h  3783  suctr  4666  ssimaexg  5790  riotasv  6598  dfsmo2  6610  omwordri  6816  3ecoptocl  6997  cfslb  8147  cofsmo  8150  cfsmolem  8151  coftr  8154  domtriomlem  8323  zorn2lem7  8383  ttukey2g  8397  gchi  8500  tskxpss  8648  tskord  8656  infm3  9968  uzind  10362  fzind  10369  fnn0ind  10370  xltnegi  10803  axdc4uz  11323  facwordi  11581  caubnd  12163  mulgcd  13047  pcfac  13269  ramz  13394  imasleval  13767  drsdir  14393  latlem  14478  psasym  14643  pstr  14644  tsrlin  14652  dirge  14683  mhmlin  14746  mhmmulg  14923  issubg2  14960  nsgbi  14972  cygabl  15501  gsumcom2  15550  dvdsrtr  15758  drnginvrcl  15853  drnginvrn0  15854  drnginvrl  15855  drnginvrr  15856  isdrngd  15861  issubrg2  15889  abvmul  15918  abvtri  15919  lmhmlin  16112  domnmuln0  16359  ipcj  16866  cssincl  16916  obsip  16949  inopn  16973  basis1  17016  iscldtop  17160  2ndcdisj  17520  cnmpt2t  17706  cnmpt22  17707  cnmptcom  17711  fbasssin  17869  ptcmplem3  18086  xmeteq0  18369  prdsxmslem2  18560  metustsym  18593  nmvs  18713  nmolb  18752  volfiniun  19442  sincosq1sgn  20407  sincosq2sgn  20408  sincosq3sgn  20409  sincosq4sgn  20410  ablocom  21874  nmcvcn  22192  ipassi  22343  htth  22422  shaddcl  22720  shmulcl  22721  shsubcl  22724  chlimi  22738  pjspansn  23080  cnopc  23417  cnfnc  23434  adj1  23437  lnfnmul  23552  atord  23892  atcvat2  23893  cdj3i  23945  pconcn  24912  shftvalg  25209  wfr3g  25538  frr3g  25582  linethru  26088  dvreasin  26291  areacirclem1  26293  ismrc  26756  fzsplit1nn0  26813  pell1234qrmulcl  26919  pell14qrmulcl  26927  stoweidlem17  27743  swrdvalodm2  28189  swrdvalodm  28190  usg2wlk  28320  cusgraisrusgra  28378  bi23impib  28569  bi13impib  28570  trelded  28653  suctrALTcf  29035  suctrALTcfVD  29036  bnj910  29320  bnj1154  29369  lsmsatcv  29809  omllaw  30042  2llnjN  30365  dalawlem10  30678  dalawlem13  30681  dalawlem14  30682  pclfinclN  30748
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator