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  3084  eqreu  3094  dedth3h  3750  ssimaexg  5756  riotasv  6564  dfsmo2  6576  omwordri  6782  3ecoptocl  6963  cfslb  8110  cofsmo  8113  cfsmolem  8114  coftr  8117  domtriomlem  8286  zorn2lem7  8346  ttukey2g  8360  gchi  8463  tskxpss  8611  tskord  8619  infm3  9931  uzind  10325  fzind  10332  fnn0ind  10333  xltnegi  10766  axdc4uz  11285  facwordi  11543  caubnd  12125  mulgcd  13009  pcfac  13231  ramz  13356  imasleval  13729  drsdir  14355  latlem  14440  psasym  14605  pstr  14606  tsrlin  14614  dirge  14645  mhmlin  14708  mhmmulg  14885  issubg2  14922  nsgbi  14934  cygabl  15463  gsumcom2  15512  dvdsrtr  15720  drnginvrcl  15815  drnginvrn0  15816  drnginvrl  15817  drnginvrr  15818  isdrngd  15823  issubrg2  15851  abvmul  15880  abvtri  15881  lmhmlin  16074  domnmuln0  16321  ipcj  16828  cssincl  16878  obsip  16911  inopn  16935  basis1  16978  iscldtop  17122  2ndcdisj  17480  cnmpt2t  17666  cnmpt22  17667  cnmptcom  17671  fbasssin  17829  ptcmplem3  18046  xmeteq0  18329  prdsxmslem2  18520  metustsym  18553  nmvs  18673  nmolb  18712  volfiniun  19402  sincosq1sgn  20367  sincosq2sgn  20368  sincosq3sgn  20369  sincosq4sgn  20370  ablocom  21834  nmcvcn  22152  ipassi  22303  htth  22382  shaddcl  22680  shmulcl  22681  shsubcl  22684  chlimi  22698  pjspansn  23040  cnopc  23377  cnfnc  23394  adj1  23397  lnfnmul  23512  atord  23852  atcvat2  23853  cdj3i  23905  pconcn  24872  shftvalg  25169  wfr3g  25477  frr3g  25502  linethru  25999  dvreasin  26187  areacirclem2  26189  ismrc  26653  fzsplit1nn0  26710  pell1234qrmulcl  26816  pell14qrmulcl  26824  stoweidlem17  27641  usg2wlk  28057  bi23impib  28290  bi13impib  28291  trelded  28371  suctrALTcf  28752  suctrALTcfVD  28753  bnj910  29037  bnj1154  29086  lsmsatcv  29505  omllaw  29738  2llnjN  30061  dalawlem10  30374  dalawlem13  30377  dalawlem14  30378  pclfinclN  30444
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