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

Theorem simp3bi 1011
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 1008 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  limuni  4927  smores2  7017  ersym  7315  ertr  7318  fvixp  7467  undifixp  7498  fiint  7789  winalim2  9063  inar1  9142  supmullem1  10504  supmullem2  10505  supmul  10506  eluzle  11094  ico01fl0  11935  ef01bndlem  14001  sin01bnd  14002  cos01bnd  14003  sin01gt0  14007  divalglem6  14140  gznegcl  14537  gzcjcl  14538  gzaddcl  14539  gzmulcl  14540  gzabssqcl  14543  4sqlem4a  14553  prdsbasprj  14961  xpsff1o  15057  mreintcl  15084  drsdir  15763  subggrp  16403  pmtrfconj  16690  symggen  16694  psgnunilem1  16717  subgpgp  16816  slwispgp  16830  sylow2alem1  16836  oppglsm  16861  efgsdmi  16949  efgsrel  16951  efgsp1  16954  efgsres  16955  efgcpbllemb  16972  efgcpbl  16973  srgi  17358  srgrz  17372  srglz  17373  ringi  17406  ringsrg  17432  irredmul  17553  lmodlema  17712  lsscl  17784  phllmhm  18840  ipcj  18842  ipeq0  18846  ocvi  18873  obsip  18925  obsocv  18930  2ndcctbss  20122  locfinnei  20190  fclssscls  20685  tmdcn  20748  tgpinv  20750  trgtmd  20833  tdrgunit  20835  ngpds  21289  elii1  21601  elii2  21602  icopnfcnv  21608  icopnfhmeo  21609  iccpnfhmeo  21611  xrhmeo  21612  phtpcer  21661  pcoass  21690  clmsubrg  21732  cphnmfval  21805  bnsca  21944  uc1pldg  22715  mon1pldg  22716  sinq12ge0  23067  cosq14gt0  23069  cosq14ge0  23070  sinord  23087  recosf1o  23088  resinf1o  23089  logrnaddcl  23128  logimul  23167  dvlog2lem  23201  atanf  23408  atanneg  23435  atancj  23438  efiatan  23440  atanlogaddlem  23441  atanlogadd  23442  atanlogsub  23444  efiatan2  23445  2efiatan  23446  ressatans  23462  dvatan  23463  areaf  23489  harmonicubnd  23537  harmonicbnd4  23538  2sqlem2  23837  2sqlem3  23839  dchrvmasumiflem1  23884  pntpbnd2  23970  f1otrg  24376  f1otrge  24377  brbtwn2  24410  ax5seglem3  24436  axpaschlem  24445  axcontlem7  24475  subgores  25504  hstel2  27336  stle1  27342  stj  27352  xrge0adddir  27916  omndadd  27930  slmdlema  27980  lmodslmd  27981  orngmul  28028  xrge0iifcnv  28150  xrge0iifiso  28152  xrge0iifhom  28154  rrextcusp  28220  rrextust  28223  sibfinima  28545  eulerpartlemf  28573  eulerpartlemgvv  28579  lgamgulmlem2  28836  snmlflim  29041  msrval  29162  mclsssvlem  29186  mclsind  29194  cntotbnd  30532  heiborlem8  30554  dmnnzd  30712  kelac1  31248  binomcxplemcvg  31500  binomcxplemnotnn0  31502  stoweidlem39  32060  stoweidlem60  32081  fourierdlem40  32168  fourierdlem78  32206  isringrng  32941  bnj563  34201  bnj1366  34289  bnj1379  34290  bnj554  34358  bnj557  34360  bnj570  34364  bnj594  34371  bnj1001  34417  bnj1006  34418  bnj1097  34438  bnj1177  34463  bnj1388  34490  bnj1398  34491  bnj1450  34507  bnj1501  34524  bnj1523  34528  atlex  35438
  Copyright terms: Public domain W3C validator