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

Theorem simp2bi 971
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
simp2bi  |-  ( ph  ->  ch )

Proof of Theorem simp2bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 186 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 968 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  smodm  6384  abianfplem  6486  erdm  6686  ixpfn  6838  winafp  8335  inar1  8413  inatsk  8416  tskuni  8421  grur1  8458  supmullem1  9736  supmullem2  9737  supmul  9738  eluzelz  10254  elfz3nn0  10839  swrds2  11576  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  sin01gt0  12486  bitsss  12633  smueqlem  12697  gznegcl  12998  gzcjcl  12999  gzaddcl  13000  gzmulcl  13001  gzabssqcl  13004  4sqlem4a  13014  structcnvcnv  13175  structfun  13176  xpsff1o  13486  mre1cl  13512  drsbn0  14087  subgss  14638  pgpgrp  14921  slwsubg  14937  efgs1b  15061  efgsp1  15062  efgsres  15063  efgredeu  15077  efgred2  15078  efgcpbllemb  15080  rngmgp  15363  irrednu  15503  lmodrng  15651  lmodprop2d  15703  lssn0  15714  phlsrng  16551  ocvss  16586  obsss  16640  fclsfil  17721  tmdtps  17775  tgptmd  17778  trgrng  17869  tdrgdrng  17872  ngpms  18138  icopnfcnv  18456  xrhmeo  18460  oprpiece1res2  18466  phtpcer  18509  pcoval2  18530  pcoass  18538  clmsca  18579  cphsqrcl  18636  bncms  18782  itg2ge0  19106  uc1pn0  19547  mon1pn0  19548  sinq12ge0  19892  cosq14gt0  19894  cosq14ge0  19895  sinord  19912  recosf1o  19913  resinf1o  19914  logrnaddcl  19947  atanf  20192  atanneg  20219  atancj  20222  efiatan  20224  atanlogaddlem  20225  atanlogadd  20226  atanlogsub  20228  efiatan2  20229  2efiatan  20230  tanatan  20231  dvatan  20247  areambl  20269  rlimcnp  20276  emgt0  20316  harmoniclbnd  20318  harmonicbnd4  20320  2sqlem2  20619  2sqlem3  20621  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  logdivbnd  20721  pntpbnd2  20752  pnt  20779  subgores  20987  subgoid  20990  subgoinv  20991  subgoablo  20994  ghsubgolem  21053  hst1a  22814  stge0  22820  sthil  22830  elunitge0  23298  xrge0iifcnv  23330  xrge0iifcv  23331  xrge0iifiso  23332  fsumrp0cl  23349  dfon2lem1  24210  dfrdg2  24223  brbtwn2  24605  ax5seglem3  24631  ax5seglem6  24634  axpaschlem  24640  axcontlem2  24665  axcontlem4  24667  itg2addnclem  25003  locfinbas  26404  cntotbnd  26623  heiborlem5  26642  heiborlem6  26643  psgnunilem5  27520  stoweidlem60  27912  bnj563  29088  bnj1212  29148  bnj1219  29149  bnj1366  29178  bnj1379  29179  bnj545  29243  bnj594  29260  bnj1118  29330  bnj1177  29352  bnj1190  29354  bnj1398  29380  bnj1417  29387  bnj1450  29396  bnj1312  29404  bnj1523  29417  atl0cl  30115  dalem-ccly  30496
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