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  4467  smores2  6387  smofvon2  6389  smofvon  6392  errel  6685  lincmb01cmp  10793  iccf1o  10794  elfznn0  10838  elfzouz  10895  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  sin01gt0  12486  cos01gt0  12487  sin02gt0  12488  smueqlem  12697  gzcn  12995  mresspw  13510  drsprs  14086  ipodrscl  14281  subgrcl  14642  pgpprm  14920  slwprm  14936  efgsdmi  15057  efgsrel  15059  efgs1b  15061  efgsp1  15062  efgsres  15063  efgsfo  15064  efgredlema  15065  efgredlemf  15066  efgredlemd  15069  efgredlemc  15070  efgredlem  15072  efgrelexlemb  15075  efgcpbllemb  15080  rnggrp  15362  irredcl  15502  lmodgrp  15650  lssss  15710  phllvec  16549  obsrcl  16639  fclstop  17722  tmdmnd  17774  tgpgrp  17777  trgtgp  17866  tdrgtrg  17871  ngpgrp  18137  elii1  18449  elii2  18450  icopnfcnv  18456  icopnfhmeo  18457  iccpnfhmeo  18459  xrhmeo  18460  oprpiece1res1  18465  oprpiece1res2  18466  phtpcer  18509  pcoval2  18530  pcoass  18538  clmlmod  18581  cphphl  18623  cphnlm  18624  cphsca  18631  bnnvc  18778  vitalilem4  18982  uc1pcl  19545  mon1pcl  19546  sinq12ge0  19892  cosq14ge0  19895  cosord  19910  cos11  19911  recosf1o  19913  resinf1o  19914  efifo  19925  logrncn  19936  atanf  20192  atanneg  20219  efiatan  20224  atanlogaddlem  20225  atanlogadd  20226  atanlogsub  20228  efiatan2  20229  2efiatan  20230  tanatan  20231  areass  20270  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  subgores  20987  subgoid  20990  subgoinv  20991  sticl  22811  hstcl  22813  bcm1n  23048  elunitrn  23296  xrge0iifiso  23332  brbtwn2  24605  ax5seglem1  24628  ax5seglem2  24629  ax5seglem3  24631  ax5seglem5  24633  ax5seglem6  24634  ax5seglem9  24637  ax5seg  24638  axbtwnid  24639  axpaschlem  24640  axpasch  24641  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  locfintop  26403  pmtrfconj  27510  stoweidlem60  27912  bnj564  29089  bnj1366  29178  bnj545  29243  bnj548  29245  bnj558  29250  bnj570  29253  bnj580  29261  bnj929  29284  bnj998  29304  bnj1006  29307  bnj1190  29354  bnj1523  29417  atllat  30112
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