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

Theorem 3impib 1150
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 1146 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 935
This theorem is referenced by:  mob  3033  eqreu  3043  dedth3h  3697  ssimaexg  5692  riotasv  6494  dfsmo2  6506  omwordri  6712  3ecoptocl  6893  cfslb  8039  cofsmo  8042  cfsmolem  8043  coftr  8046  domtriomlem  8215  zorn2lem7  8276  ttukey2g  8290  gchi  8393  tskxpss  8541  tskord  8549  infm3  9860  uzind  10254  fzind  10261  fnn0ind  10262  xltnegi  10695  axdc4uz  11209  facwordi  11467  caubnd  12049  mulgcd  12933  pcfac  13155  ramz  13280  imasleval  13653  drsdir  14279  latlem  14364  psasym  14529  pstr  14530  tsrlin  14538  dirge  14569  mhmlin  14632  mhmmulg  14809  issubg2  14846  nsgbi  14858  cygabl  15387  gsumcom2  15436  dvdsrtr  15644  drnginvrcl  15739  drnginvrn0  15740  drnginvrl  15741  drnginvrr  15742  isdrngd  15747  issubrg2  15775  abvmul  15804  abvtri  15805  lmhmlin  16002  domnmuln0  16249  ipcj  16755  cssincl  16805  obsip  16838  inopn  16862  basis1  16905  iscldtop  17049  2ndcdisj  17399  cnmpt2t  17584  cnmpt22  17585  cnmptcom  17589  fbasssin  17744  ptcmplem3  17961  xmeteq0  18116  prdsxmslem2  18288  nmvs  18400  nmolb  18439  volfiniun  19119  sincosq1sgn  20084  sincosq2sgn  20085  sincosq3sgn  20086  sincosq4sgn  20087  ablocom  21263  nmcvcn  21581  ipassi  21732  htth  21811  shaddcl  22109  shmulcl  22110  shsubcl  22113  chlimi  22127  pjspansn  22469  cnopc  22806  cnfnc  22823  adj1  22826  lnfnmul  22941  atord  23281  atcvat2  23282  cdj3i  23334  abfmpeld  23468  metustsym  23798  pconcn  24358  shftvalg  24692  wfr3g  24996  frr3g  25021  linethru  25518  dvreasin  25698  areacirclem2  25700  ismrc  26282  fzsplit1nn0  26339  pell1234qrmulcl  26446  pell14qrmulcl  26454  stoweidlem17  27272  bi23impib  27997  bi13impib  27998  bi123impib  27999  trelded  28078  suctrALTcf  28462  suctrALTcfVD  28463  suctrALT4  28468  bnj910  28744  bnj1154  28793  a12study4  29188  lsmsatcv  29271  omllaw  29504  2llnjN  29827  dalawlem10  30140  dalawlem13  30143  dalawlem14  30144  pclfinclN  30210
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 937
  Copyright terms: Public domain W3C validator