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

Theorem simp3bi 974
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 187 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp3d 971 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  limuni  4641  smores2  6616  ersym  6917  ertr  6920  fvixp  7067  undifixp  7098  fiint  7383  winalim2  8571  inar1  8650  supmullem1  9974  supmullem2  9975  supmul  9976  eluzle  10498  ef01bndlem  12785  sin01bnd  12786  cos01bnd  12787  sin01gt0  12791  divalglem6  12918  gznegcl  13303  gzcjcl  13304  gzaddcl  13305  gzmulcl  13306  gzabssqcl  13309  4sqlem4a  13319  prdsbasprj  13694  xpsff1o  13793  mreintcl  13820  drsdir  14392  subggrp  14947  subgpgp  15231  slwispgp  15245  sylow2alem1  15251  oppglsm  15276  efgsdmi  15364  efgsrel  15366  efgsp1  15369  efgsres  15370  efgcpbllemb  15387  efgcpbl  15388  rngi  15676  irredmul  15814  lmodlema  15955  lsscl  16019  phllmhm  16863  ipcj  16865  ipeq0  16869  ocvi  16896  obsip  16948  obsocv  16953  2ndcctbss  17518  fclssscls  18050  tmdcn  18113  tgpinv  18115  trgtmd  18194  tdrgunit  18196  ngpds  18650  elii1  18960  elii2  18961  icopnfcnv  18967  icopnfhmeo  18968  iccpnfhmeo  18970  xrhmeo  18971  phtpcer  19020  pcoass  19049  clmsubrg  19091  cphnmfval  19155  bnsca  19292  uc1pldg  20071  mon1pldg  20072  sinq12ge0  20416  cosq14gt0  20418  cosq14ge0  20419  sinord  20436  recosf1o  20437  resinf1o  20438  logrnaddcl  20472  logimul  20509  dvlog2lem  20543  atanf  20720  atanneg  20747  atancj  20750  efiatan  20752  atanlogaddlem  20753  atanlogadd  20754  atanlogsub  20756  efiatan2  20757  2efiatan  20758  ressatans  20774  dvatan  20775  areaf  20800  harmonicubnd  20848  harmonicbnd4  20849  2sqlem2  21148  2sqlem3  21150  dchrvmasumiflem1  21195  pntpbnd2  21281  subgores  21892  hstel2  23722  stle1  23728  stj  23738  xrge0adddir  24215  ofldadd  24238  ofldmul  24239  xrge0iifcnv  24319  xrge0iifiso  24321  xrge0iifhom  24323  lgamgulmlem2  24814  snmlflim  25019  brbtwn2  25844  ax5seglem3  25870  axpaschlem  25879  axcontlem7  25909  locfinnei  26382  cntotbnd  26505  heiborlem8  26527  dmnnzd  26685  kelac1  27138  pmtrfconj  27384  symggen  27388  psgnunilem1  27393  stoweidlem39  27764  stoweidlem60  27785  bnj563  29111  bnj1366  29201  bnj1379  29202  bnj554  29270  bnj557  29272  bnj570  29276  bnj594  29283  bnj1001  29329  bnj1006  29330  bnj1097  29350  bnj1177  29375  bnj1388  29402  bnj1398  29403  bnj1450  29419  bnj1501  29436  bnj1523  29440  atlex  30114
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