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

Theorem simp3bi 1013
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 1010 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973
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 975
This theorem is referenced by:  limuni  4938  smores2  7026  ersym  7324  ertr  7327  fvixp  7475  undifixp  7506  fiint  7798  winalim2  9075  inar1  9154  supmullem1  10510  supmullem2  10511  supmul  10512  eluzle  11095  ef01bndlem  13783  sin01bnd  13784  cos01bnd  13785  sin01gt0  13789  divalglem6  13918  gznegcl  14315  gzcjcl  14316  gzaddcl  14317  gzmulcl  14318  gzabssqcl  14321  4sqlem4a  14331  prdsbasprj  14730  xpsff1o  14826  mreintcl  14853  drsdir  15425  subggrp  16018  pmtrfconj  16306  symggen  16310  psgnunilem1  16333  subgpgp  16432  slwispgp  16446  sylow2alem1  16452  oppglsm  16477  efgsdmi  16565  efgsrel  16567  efgsp1  16570  efgsres  16571  efgcpbllemb  16588  efgcpbl  16589  srgi  16977  srgrz  16991  srglz  16992  rngi  17024  irredmul  17171  lmodlema  17329  lsscl  17401  phllmhm  18474  ipcj  18476  ipeq0  18480  ocvi  18507  obsip  18559  obsocv  18564  2ndcctbss  19762  locfinnei  19852  fclssscls  20346  tmdcn  20409  tgpinv  20411  trgtmd  20494  tdrgunit  20496  ngpds  20950  elii1  21262  elii2  21263  icopnfcnv  21269  icopnfhmeo  21270  iccpnfhmeo  21272  xrhmeo  21273  phtpcer  21322  pcoass  21351  clmsubrg  21393  cphnmfval  21466  bnsca  21605  uc1pldg  22376  mon1pldg  22377  sinq12ge0  22726  cosq14gt0  22728  cosq14ge0  22729  sinord  22746  recosf1o  22747  resinf1o  22748  logrnaddcl  22787  logimul  22824  dvlog2lem  22858  atanf  23036  atanneg  23063  atancj  23066  efiatan  23068  atanlogaddlem  23069  atanlogadd  23070  atanlogsub  23072  efiatan2  23073  2efiatan  23074  ressatans  23090  dvatan  23091  areaf  23116  harmonicubnd  23164  harmonicbnd4  23165  2sqlem2  23464  2sqlem3  23466  dchrvmasumiflem1  23511  pntpbnd2  23597  f1otrg  23947  f1otrge  23948  brbtwn2  23981  ax5seglem3  24007  axpaschlem  24016  axcontlem7  24046  subgores  25079  hstel2  26911  stle1  26917  stj  26927  xrge0adddir  27441  omndadd  27455  slmdlema  27505  lmodslmd  27506  orngmul  27553  xrge0iifcnv  27666  xrge0iifiso  27668  xrge0iifhom  27670  rrextcusp  27737  rrextust  27740  sibfinima  28032  eulerpartlemf  28060  eulerpartlemgvv  28066  lgamgulmlem2  28323  snmlflim  28528  msrval  28649  mclsssvlem  28673  mclsind  28681  cntotbnd  30122  heiborlem8  30144  dmnnzd  30302  kelac1  30840  elfzfzo  31262  stoweidlem39  31566  stoweidlem60  31587  fourierdlem40  31674  fourierdlem78  31712  bnj563  33096  bnj1366  33184  bnj1379  33185  bnj554  33253  bnj557  33255  bnj570  33259  bnj594  33266  bnj1001  33312  bnj1006  33313  bnj1097  33333  bnj1177  33358  bnj1388  33385  bnj1398  33386  bnj1450  33402  bnj1501  33419  bnj1523  33423  bj-flbi3  33896  atlex  34330
  Copyright terms: Public domain W3C validator