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

Theorem simp3bi 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
simp3bi  |-  ( ph  ->  th )

Proof of Theorem simp3bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 186 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp3d 969 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
This theorem is referenced by:  limuni  4452  smores2  6371  ersym  6672  ertr  6675  fvixp  6821  undifixp  6852  fiint  7133  winalim2  8318  inar1  8397  supmullem1  9720  supmullem2  9721  supmul  9722  eluzle  10240  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  sin01gt0  12470  divalglem6  12597  gznegcl  12982  gzcjcl  12983  gzaddcl  12984  gzmulcl  12985  gzabssqcl  12988  4sqlem4a  12998  prdsbasprj  13371  xpsff1o  13470  mreintcl  13497  drsdir  14069  subggrp  14624  subgpgp  14908  slwispgp  14922  sylow2alem1  14928  oppglsm  14953  efgsdmi  15041  efgsrel  15043  efgsp1  15046  efgsres  15047  efgcpbllemb  15064  efgcpbl  15065  rngi  15353  irredmul  15491  lmodlema  15632  lsscl  15700  phllmhm  16536  ipcj  16538  ipeq0  16542  ocvi  16569  obsip  16621  obsocv  16626  2ndcctbss  17181  fclssscls  17713  tmdcn  17766  tgpinv  17768  trgtmd  17847  tdrgunit  17849  ngpds  18125  elii1  18433  elii2  18434  icopnfcnv  18440  icopnfhmeo  18441  iccpnfhmeo  18443  xrhmeo  18444  phtpcer  18493  pcoass  18522  clmsubrg  18564  cphnmfval  18628  bnsca  18761  uc1pldg  19534  mon1pldg  19535  sinq12ge0  19876  cosq14gt0  19878  cosq14ge0  19879  sinord  19896  recosf1o  19897  resinf1o  19898  logrnaddcl  19931  logimul  19968  dvlog2lem  19999  atanf  20176  atanneg  20203  atancj  20206  efiatan  20208  atanlogaddlem  20209  atanlogadd  20210  atanlogsub  20212  efiatan2  20213  2efiatan  20214  ressatans  20230  dvatan  20231  areaf  20256  harmonicubnd  20303  harmonicbnd4  20304  2sqlem2  20603  2sqlem3  20605  dchrvmasumiflem1  20650  pntpbnd2  20736  subgores  20971  hstel2  22799  stle1  22805  stj  22815  iistmd  23286  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0adddir  23332  snmlflim  23915  brbtwn2  24533  ax5seglem3  24559  axpaschlem  24568  axcontlem7  24598  tethpnc  26070  locfinnei  26302  cntotbnd  26520  heiborlem8  26542  dmnnzd  26700  kelac1  27161  pmtrfconj  27407  symggen  27411  psgnunilem1  27416  stoweidlem39  27788  stoweidlem60  27809  bnj563  28772  bnj1366  28862  bnj1379  28863  bnj554  28931  bnj557  28933  bnj570  28937  bnj594  28944  bnj1001  28990  bnj1006  28991  bnj1097  29011  bnj1177  29036  bnj1388  29063  bnj1398  29064  bnj1450  29080  bnj1501  29097  bnj1523  29101  atlex  29506
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