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

Theorem 3impib 1151
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 426 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1147 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  mob  3061  eqreu  3071  dedth3h  3727  ssimaexg  5730  riotasv  6535  dfsmo2  6547  omwordri  6753  3ecoptocl  6934  cfslb  8081  cofsmo  8084  cfsmolem  8085  coftr  8088  domtriomlem  8257  zorn2lem7  8317  ttukey2g  8331  gchi  8434  tskxpss  8582  tskord  8590  infm3  9901  uzind  10295  fzind  10302  fnn0ind  10303  xltnegi  10736  axdc4uz  11251  facwordi  11509  caubnd  12091  mulgcd  12975  pcfac  13197  ramz  13322  imasleval  13695  drsdir  14321  latlem  14406  psasym  14571  pstr  14572  tsrlin  14580  dirge  14611  mhmlin  14674  mhmmulg  14851  issubg2  14888  nsgbi  14900  cygabl  15429  gsumcom2  15478  dvdsrtr  15686  drnginvrcl  15781  drnginvrn0  15782  drnginvrl  15783  drnginvrr  15784  isdrngd  15789  issubrg2  15817  abvmul  15846  abvtri  15847  lmhmlin  16040  domnmuln0  16287  ipcj  16790  cssincl  16840  obsip  16873  inopn  16897  basis1  16940  iscldtop  17084  2ndcdisj  17442  cnmpt2t  17628  cnmpt22  17629  cnmptcom  17633  fbasssin  17791  ptcmplem3  18008  xmeteq0  18279  prdsxmslem2  18451  nmvs  18585  nmolb  18624  volfiniun  19310  sincosq1sgn  20275  sincosq2sgn  20276  sincosq3sgn  20277  sincosq4sgn  20278  ablocom  21723  nmcvcn  22041  ipassi  22192  htth  22271  shaddcl  22569  shmulcl  22570  shsubcl  22573  chlimi  22587  pjspansn  22929  cnopc  23266  cnfnc  23283  adj1  23286  lnfnmul  23401  atord  23741  atcvat2  23742  cdj3i  23794  pconcn  24692  shftvalg  24989  wfr3g  25281  frr3g  25306  linethru  25803  dvreasin  25982  areacirclem2  25984  ismrc  26448  fzsplit1nn0  26505  pell1234qrmulcl  26611  pell14qrmulcl  26619  stoweidlem17  27436  bi23impib  27916  bi13impib  27917  trelded  27997  suctrALTcf  28377  suctrALTcfVD  28378  bnj910  28659  bnj1154  28708  lsmsatcv  29127  omllaw  29360  2llnjN  29683  dalawlem10  29996  dalawlem13  29999  dalawlem14  30000  pclfinclN  30066
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator