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

Theorem simp3bi 1000
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 194 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp3d 997 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 960
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 962
This theorem is referenced by:  limuni  4775  smores2  6811  ersym  7109  ertr  7112  fvixp  7264  undifixp  7295  fiint  7584  winalim2  8859  inar1  8938  supmullem1  10292  supmullem2  10293  supmul  10294  eluzle  10869  ef01bndlem  13464  sin01bnd  13465  cos01bnd  13466  sin01gt0  13470  divalglem6  13598  gznegcl  13992  gzcjcl  13993  gzaddcl  13994  gzmulcl  13995  gzabssqcl  13998  4sqlem4a  14008  prdsbasprj  14406  xpsff1o  14502  mreintcl  14529  drsdir  15101  subggrp  15677  pmtrfconj  15965  symggen  15969  psgnunilem1  15992  subgpgp  16089  slwispgp  16103  sylow2alem1  16109  oppglsm  16134  efgsdmi  16222  efgsrel  16224  efgsp1  16227  efgsres  16228  efgcpbllemb  16245  efgcpbl  16246  srgi  16603  srgrz  16617  srglz  16618  rngi  16647  irredmul  16791  lmodlema  16933  lsscl  17002  phllmhm  18020  ipcj  18022  ipeq0  18026  ocvi  18053  obsip  18105  obsocv  18110  2ndcctbss  19018  fclssscls  19550  tmdcn  19613  tgpinv  19615  trgtmd  19698  tdrgunit  19700  ngpds  20154  elii1  20466  elii2  20467  icopnfcnv  20473  icopnfhmeo  20474  iccpnfhmeo  20476  xrhmeo  20477  phtpcer  20526  pcoass  20555  clmsubrg  20597  cphnmfval  20670  bnsca  20809  uc1pldg  21579  mon1pldg  21580  sinq12ge0  21929  cosq14gt0  21931  cosq14ge0  21932  sinord  21949  recosf1o  21950  resinf1o  21951  logrnaddcl  21985  logimul  22022  dvlog2lem  22056  atanf  22234  atanneg  22261  atancj  22264  efiatan  22266  atanlogaddlem  22267  atanlogadd  22268  atanlogsub  22270  efiatan2  22271  2efiatan  22272  ressatans  22288  dvatan  22289  areaf  22314  harmonicubnd  22362  harmonicbnd4  22363  2sqlem2  22662  2sqlem3  22664  dchrvmasumiflem1  22709  pntpbnd2  22795  f1otrg  23052  f1otrge  23053  brbtwn2  23086  ax5seglem3  23112  axpaschlem  23121  axcontlem7  23151  subgores  23726  hstel2  25558  stle1  25564  stj  25574  xrge0adddir  26088  omndadd  26102  slmdlema  26152  lmodslmd  26153  orngmul  26206  xrge0iifcnv  26299  xrge0iifiso  26301  xrge0iifhom  26303  rrextcusp  26370  rrextust  26373  sibfinima  26655  eulerpartlemf  26683  eulerpartlemgvv  26689  lgamgulmlem2  26946  snmlflim  27151  locfinnei  28499  cntotbnd  28620  heiborlem8  28642  dmnnzd  28800  kelac1  29341  stoweidlem39  29759  stoweidlem60  29780  bnj563  31569  bnj1366  31657  bnj1379  31658  bnj554  31726  bnj557  31728  bnj570  31732  bnj594  31739  bnj1001  31785  bnj1006  31786  bnj1097  31806  bnj1177  31831  bnj1388  31858  bnj1398  31859  bnj1450  31875  bnj1501  31892  bnj1523  31896  bj-flbi3  32256  atlex  32683
  Copyright terms: Public domain W3C validator