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

Theorem simp1bi 972
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
3simp1bi.1  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
Assertion
Ref Expression
simp1bi  |-  ( ph  ->  ps )

Proof of Theorem simp1bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 187 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp1d 969 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  limord  4632  smores2  6608  smofvon2  6610  smofvon  6613  errel  6906  lincmb01cmp  11030  iccf1o  11031  elfznn0  11075  elfzouz  11136  ef01bndlem  12777  sin01bnd  12778  cos01bnd  12779  sin01gt0  12783  cos01gt0  12784  sin02gt0  12785  smueqlem  12994  gzcn  13292  mresspw  13809  drsprs  14385  ipodrscl  14580  subgrcl  14941  pgpprm  15219  slwprm  15235  efgsdmi  15356  efgsrel  15358  efgs1b  15360  efgsp1  15361  efgsres  15362  efgsfo  15363  efgredlema  15364  efgredlemf  15365  efgredlemd  15368  efgredlemc  15369  efgredlem  15371  efgrelexlemb  15374  efgcpbllemb  15379  rnggrp  15661  irredcl  15801  lmodgrp  15949  lssss  16005  phllvec  16852  obsrcl  16942  fclstop  18035  tmdmnd  18097  tgpgrp  18100  trgtgp  18189  tdrgtrg  18194  ust0  18241  ngpgrp  18638  elii1  18952  elii2  18953  icopnfcnv  18959  icopnfhmeo  18960  iccpnfhmeo  18962  xrhmeo  18963  oprpiece1res1  18968  oprpiece1res2  18969  phtpcer  19012  pcoval2  19033  pcoass  19041  clmlmod  19084  cphphl  19126  cphnlm  19127  cphsca  19134  bnnvc  19285  uc1pcl  20058  mon1pcl  20059  sinq12ge0  20408  cosq14ge0  20411  cosord  20426  cos11  20427  recosf1o  20429  resinf1o  20430  efifo  20441  logrncn  20452  atanf  20712  atanneg  20739  efiatan  20744  atanlogaddlem  20745  atanlogadd  20746  atanlogsub  20748  efiatan2  20749  2efiatan  20750  tanatan  20751  areass  20790  dchrvmasumlem2  21184  dchrvmasumiflem1  21187  subgores  21884  subgoid  21887  subgoinv  21888  sticl  23710  hstcl  23712  ofldfld  24228  elunitrn  24287  brbtwn2  25836  ax5seglem1  25859  ax5seglem2  25860  ax5seglem3  25862  ax5seglem5  25864  ax5seglem6  25865  ax5seglem9  25868  ax5seg  25869  axbtwnid  25870  axpaschlem  25871  axpasch  25872  axcontlem2  25896  axcontlem4  25898  axcontlem7  25901  locfintop  26371  pmtrfconj  27375  stoweidlem60  27776  2spotiundisj  28388  bnj564  29049  bnj1366  29138  bnj545  29203  bnj548  29205  bnj558  29210  bnj570  29213  bnj580  29221  bnj929  29244  bnj998  29264  bnj1006  29267  bnj1190  29314  bnj1523  29377  atllat  30035
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