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  4633  smores2  6608  ersym  6909  ertr  6912  fvixp  7059  undifixp  7090  fiint  7375  winalim2  8563  inar1  8642  supmullem1  9966  supmullem2  9967  supmul  9968  eluzle  10490  ef01bndlem  12777  sin01bnd  12778  cos01bnd  12779  sin01gt0  12783  divalglem6  12910  gznegcl  13295  gzcjcl  13296  gzaddcl  13297  gzmulcl  13298  gzabssqcl  13301  4sqlem4a  13311  prdsbasprj  13686  xpsff1o  13785  mreintcl  13812  drsdir  14384  subggrp  14939  subgpgp  15223  slwispgp  15237  sylow2alem1  15243  oppglsm  15268  efgsdmi  15356  efgsrel  15358  efgsp1  15361  efgsres  15362  efgcpbllemb  15379  efgcpbl  15380  rngi  15668  irredmul  15806  lmodlema  15947  lsscl  16011  phllmhm  16855  ipcj  16857  ipeq0  16861  ocvi  16888  obsip  16940  obsocv  16945  2ndcctbss  17510  fclssscls  18042  tmdcn  18105  tgpinv  18107  trgtmd  18186  tdrgunit  18188  ngpds  18642  elii1  18952  elii2  18953  icopnfcnv  18959  icopnfhmeo  18960  iccpnfhmeo  18962  xrhmeo  18963  phtpcer  19012  pcoass  19041  clmsubrg  19083  cphnmfval  19147  bnsca  19284  uc1pldg  20063  mon1pldg  20064  sinq12ge0  20408  cosq14gt0  20410  cosq14ge0  20411  sinord  20428  recosf1o  20429  resinf1o  20430  logrnaddcl  20464  logimul  20501  dvlog2lem  20535  atanf  20712  atanneg  20739  atancj  20742  efiatan  20744  atanlogaddlem  20745  atanlogadd  20746  atanlogsub  20748  efiatan2  20749  2efiatan  20750  ressatans  20766  dvatan  20767  areaf  20792  harmonicubnd  20840  harmonicbnd4  20841  2sqlem2  21140  2sqlem3  21142  dchrvmasumiflem1  21187  pntpbnd2  21273  subgores  21884  hstel2  23714  stle1  23720  stj  23730  xrge0adddir  24207  ofldadd  24230  ofldmul  24231  xrge0iifcnv  24311  xrge0iifiso  24313  xrge0iifhom  24315  lgamgulmlem2  24806  snmlflim  25011  brbtwn2  25836  ax5seglem3  25862  axpaschlem  25871  axcontlem7  25901  locfinnei  26373  cntotbnd  26496  heiborlem8  26518  dmnnzd  26676  kelac1  27129  pmtrfconj  27375  symggen  27379  psgnunilem1  27384  stoweidlem39  27755  stoweidlem60  27776  bnj563  29048  bnj1366  29138  bnj1379  29139  bnj554  29207  bnj557  29209  bnj570  29213  bnj594  29220  bnj1001  29266  bnj1006  29267  bnj1097  29287  bnj1177  29312  bnj1388  29339  bnj1398  29340  bnj1450  29356  bnj1501  29373  bnj1523  29377  atlex  30051
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