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  3118  eqreu  3128  dedth3h  3784  suctr  4668  ssimaexg  5792  riotasv  6600  dfsmo2  6612  omwordri  6818  3ecoptocl  6999  cfslb  8151  cofsmo  8154  cfsmolem  8155  coftr  8158  domtriomlem  8327  zorn2lem7  8387  ttukey2g  8401  gchi  8504  tskxpss  8652  tskord  8660  infm3  9972  uzind  10366  fzind  10373  fnn0ind  10374  xltnegi  10807  axdc4uz  11327  facwordi  11585  caubnd  12167  mulgcd  13051  pcfac  13273  ramz  13398  imasleval  13771  drsdir  14397  latlem  14482  psasym  14647  pstr  14648  tsrlin  14656  dirge  14687  mhmlin  14750  mhmmulg  14927  issubg2  14964  nsgbi  14976  cygabl  15505  gsumcom2  15554  dvdsrtr  15762  drnginvrcl  15857  drnginvrn0  15858  drnginvrl  15859  drnginvrr  15860  isdrngd  15865  issubrg2  15893  abvmul  15922  abvtri  15923  lmhmlin  16116  domnmuln0  16363  ipcj  16870  cssincl  16920  obsip  16953  inopn  16977  basis1  17020  iscldtop  17164  2ndcdisj  17524  cnmpt2t  17710  cnmpt22  17711  cnmptcom  17715  fbasssin  17873  ptcmplem3  18090  xmeteq0  18373  prdsxmslem2  18564  metustsym  18597  nmvs  18717  nmolb  18756  volfiniun  19446  sincosq1sgn  20411  sincosq2sgn  20412  sincosq3sgn  20413  sincosq4sgn  20414  ablocom  21878  nmcvcn  22196  ipassi  22347  htth  22426  shaddcl  22724  shmulcl  22725  shsubcl  22728  chlimi  22742  pjspansn  23084  cnopc  23421  cnfnc  23438  adj1  23441  lnfnmul  23556  atord  23896  atcvat2  23897  cdj3i  23949  pconcn  24916  shftvalg  25213  wfr3g  25542  frr3g  25586  linethru  26092  sin2h  26250  cos2h  26251  tan2h  26252  dvreasin  26304  areacirclem1  26306  ismrc  26769  fzsplit1nn0  26826  pell1234qrmulcl  26932  pell14qrmulcl  26940  stoweidlem17  27756  swrdvalodm2  28222  swrdvalodm  28223  usg2wlk  28357  cusgraisrusgra  28449  bi23impib  28642  bi13impib  28643  trelded  28726  suctrALTcf  29108  suctrALTcfVD  29109  bnj910  29393  bnj1154  29442  lsmsatcv  29882  omllaw  30115  2llnjN  30438  dalawlem10  30751  dalawlem13  30754  dalawlem14  30755  pclfinclN  30821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator