MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3impib Structured version   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  3108  eqreu  3118  dedth3h  3774  suctr  4657  ssimaexg  5781  riotasv  6589  dfsmo2  6601  omwordri  6807  3ecoptocl  6988  cfslb  8136  cofsmo  8139  cfsmolem  8140  coftr  8143  domtriomlem  8312  zorn2lem7  8372  ttukey2g  8386  gchi  8489  tskxpss  8637  tskord  8645  infm3  9957  uzind  10351  fzind  10358  fnn0ind  10359  xltnegi  10792  axdc4uz  11312  facwordi  11570  caubnd  12152  mulgcd  13036  pcfac  13258  ramz  13383  imasleval  13756  drsdir  14382  latlem  14467  psasym  14632  pstr  14633  tsrlin  14641  dirge  14672  mhmlin  14735  mhmmulg  14912  issubg2  14949  nsgbi  14961  cygabl  15490  gsumcom2  15539  dvdsrtr  15747  drnginvrcl  15842  drnginvrn0  15843  drnginvrl  15844  drnginvrr  15845  isdrngd  15850  issubrg2  15878  abvmul  15907  abvtri  15908  lmhmlin  16101  domnmuln0  16348  ipcj  16855  cssincl  16905  obsip  16938  inopn  16962  basis1  17005  iscldtop  17149  2ndcdisj  17509  cnmpt2t  17695  cnmpt22  17696  cnmptcom  17700  fbasssin  17858  ptcmplem3  18075  xmeteq0  18358  prdsxmslem2  18549  metustsym  18582  nmvs  18702  nmolb  18741  volfiniun  19431  sincosq1sgn  20396  sincosq2sgn  20397  sincosq3sgn  20398  sincosq4sgn  20399  ablocom  21863  nmcvcn  22181  ipassi  22332  htth  22411  shaddcl  22709  shmulcl  22710  shsubcl  22713  chlimi  22727  pjspansn  23069  cnopc  23406  cnfnc  23423  adj1  23426  lnfnmul  23541  atord  23881  atcvat2  23882  cdj3i  23934  pconcn  24901  shftvalg  25198  wfr3g  25522  frr3g  25546  linethru  26052  dvreasin  26243  areacirclem2  26245  ismrc  26709  fzsplit1nn0  26766  pell1234qrmulcl  26872  pell14qrmulcl  26880  stoweidlem17  27697  swrdvalodm2  28124  swrdvalodm  28125  usg2wlk  28236  bi23impib  28469  bi13impib  28470  trelded  28553  suctrALTcf  28935  suctrALTcfVD  28936  bnj910  29220  bnj1154  29269  lsmsatcv  29709  omllaw  29942  2llnjN  30265  dalawlem10  30578  dalawlem13  30581  dalawlem14  30582  pclfinclN  30648
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