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

Theorem simp1bi 970
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 186 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp1d 967 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  limord  4451  smores2  6371  smofvon2  6373  smofvon  6376  errel  6669  lincmb01cmp  10777  iccf1o  10778  elfznn0  10822  elfzouz  10879  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  sin01gt0  12470  cos01gt0  12471  sin02gt0  12472  smueqlem  12681  gzcn  12979  mresspw  13494  drsprs  14070  ipodrscl  14265  subgrcl  14626  pgpprm  14904  slwprm  14920  efgsdmi  15041  efgsrel  15043  efgs1b  15045  efgsp1  15046  efgsres  15047  efgsfo  15048  efgredlema  15049  efgredlemf  15050  efgredlemd  15053  efgredlemc  15054  efgredlem  15056  efgrelexlemb  15059  efgcpbllemb  15064  rnggrp  15346  irredcl  15486  lmodgrp  15634  lssss  15694  phllvec  16533  obsrcl  16623  fclstop  17706  tmdmnd  17758  tgpgrp  17761  trgtgp  17850  tdrgtrg  17855  ngpgrp  18121  elii1  18433  elii2  18434  icopnfcnv  18440  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  oprpiece1res1  18449  oprpiece1res2  18450  phtpcer  18493  pcoval2  18514  pcoass  18522  clmlmod  18565  cphphl  18607  cphnlm  18608  cphsca  18615  bnnvc  18762  vitalilem4  18966  uc1pcl  19529  mon1pcl  19530  sinq12ge0  19876  cosq14ge0  19879  cosord  19894  cos11  19895  recosf1o  19897  resinf1o  19898  efifo  19909  logrncn  19920  atanf  20176  atanneg  20203  efiatan  20208  atanlogaddlem  20209  atanlogadd  20210  atanlogsub  20212  efiatan2  20213  2efiatan  20214  tanatan  20215  areass  20254  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  subgores  20971  subgoid  20974  subgoinv  20975  sticl  22795  hstcl  22797  bcm1n  23032  elunitrn  23281  xrge0iifiso  23317  brbtwn2  24533  ax5seglem1  24556  ax5seglem2  24557  ax5seglem3  24559  ax5seglem5  24561  ax5seglem6  24562  ax5seglem9  24565  ax5seg  24566  axbtwnid  24567  axpaschlem  24568  axpasch  24569  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  locfintop  26300  pmtrfconj  27407  stoweidlem60  27809  bnj564  28773  bnj1366  28862  bnj545  28927  bnj548  28929  bnj558  28934  bnj570  28937  bnj580  28945  bnj929  28968  bnj998  28988  bnj1006  28991  bnj1190  29038  bnj1523  29101  atllat  29490
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 936
  Copyright terms: Public domain W3C validator