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

Theorem simp3bi 1031
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 199 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp3d 1028 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  limuni  5506  smores2  7104  ersym  7406  ertr  7409  fvixp  7558  undifixp  7589  fiint  7879  winalim2  9152  inar1  9231  supmullem1  10610  supmullem2  10611  supmul  10612  eluzle  11205  ico01fl0  12091  ef01bndlem  14293  sin01bnd  14294  cos01bnd  14295  sin01gt0  14299  divalglem6  14433  gznegcl  14934  gzcjcl  14935  gzaddcl  14936  gzmulcl  14937  gzabssqcl  14940  4sqlem4a  14950  prdsbasprj  15425  xpsff1o  15529  mreintcl  15556  drsdir  16235  subggrp  16875  pmtrfconj  17162  symggen  17166  psgnunilem1  17189  subgpgp  17304  slwispgp  17318  sylow2alem1  17324  oppglsm  17349  efgsdmi  17437  efgsrel  17439  efgsp1  17442  efgsres  17443  efgcpbllemb  17460  efgcpbl  17461  srgi  17800  srgrz  17814  srglz  17815  ringi  17848  ringsrg  17874  irredmul  17992  lmodlema  18151  lsscl  18221  phllmhm  19254  ipcj  19256  ipeq0  19260  ocvi  19287  obsip  19339  obsocv  19344  2ndcctbss  20525  locfinnei  20593  fclssscls  21088  tmdcn  21153  tgpinv  21155  trgtmd  21234  tdrgunit  21236  ngpds  21672  elii1  22018  elii2  22019  icopnfcnv  22025  icopnfhmeo  22026  iccpnfhmeo  22028  xrhmeo  22029  phtpcer  22081  pcoass  22110  clmsubrg  22152  cphnmfval  22225  bnsca  22362  uc1pldg  23155  mon1pldg  23156  sinq12ge0  23519  cosq14gt0  23521  cosq14ge0  23522  sinord  23539  recosf1o  23540  resinf1o  23541  logrnaddcl  23580  logimul  23619  dvlog2lem  23653  atanf  23862  atanneg  23889  atancj  23892  efiatan  23894  atanlogaddlem  23895  atanlogadd  23896  atanlogsub  23898  efiatan2  23899  2efiatan  23900  ressatans  23916  dvatan  23917  areaf  23943  harmonicubnd  23991  harmonicbnd4  23992  lgamgulmlem2  24011  2sqlem2  24348  2sqlem3  24350  dchrvmasumiflem1  24395  pntpbnd2  24481  f1otrg  24957  f1otrge  24958  brbtwn2  24991  ax5seglem3  25017  axpaschlem  25026  axcontlem7  25056  subgores  26088  hstel2  27928  stle1  27934  stj  27944  xrge0adddir  28506  omndadd  28520  slmdlema  28570  lmodslmd  28571  orngmul  28617  xrge0iifcnv  28790  xrge0iifiso  28792  xrge0iifhom  28794  rrextcusp  28860  rrextust  28863  unelros  29044  difelros  29045  inelsros  29051  diffiunisros  29052  sibfinima  29222  eulerpartlemf  29253  eulerpartlemgvv  29259  bnj563  29603  bnj1366  29691  bnj1379  29692  bnj554  29760  bnj557  29762  bnj570  29766  bnj594  29773  bnj1001  29819  bnj1006  29820  bnj1097  29840  bnj1177  29865  bnj1388  29892  bnj1398  29893  bnj1450  29909  bnj1501  29926  bnj1523  29930  snmlflim  30105  msrval  30226  mclsssvlem  30250  mclsind  30258  ptrecube  31986  cntotbnd  32174  heiborlem8  32196  dmnnzd  32354  atlex  32928  kelac1  35967  binomcxplemcvg  36748  binomcxplemnotnn0  36750  stoweidlem39  38001  stoweidlem60  38022  fourierdlem40  38111  fourierdlem78  38149  isringrng  40250
  Copyright terms: Public domain W3C validator