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

Theorem simp2bi 973
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
simp2bi  |-  ( ph  ->  ch )

Proof of Theorem simp2bi
StepHypRef Expression
1 3simp1bi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
21biimpi 187 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
32simp2d 970 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ w3a 936
This theorem is referenced by:  smodm  6572  abianfplem  6674  erdm  6874  ixpfn  7027  winafp  8528  inar1  8606  inatsk  8609  tskuni  8614  grur1  8651  supmullem1  9930  supmullem2  9931  supmul  9932  eluzelz  10452  elfz3nn0  11040  swrds2  11835  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  sin01gt0  12746  bitsss  12893  smueqlem  12957  gznegcl  13258  gzcjcl  13259  gzaddcl  13260  gzmulcl  13261  gzabssqcl  13264  4sqlem4a  13274  structcnvcnv  13435  structfun  13436  xpsff1o  13748  mre1cl  13774  drsbn0  14349  subgss  14900  pgpgrp  15183  slwsubg  15199  efgs1b  15323  efgsp1  15324  efgsres  15325  efgredeu  15339  efgred2  15340  efgcpbllemb  15342  rngmgp  15625  irrednu  15765  lmodrng  15913  lmodprop2d  15961  lssn0  15972  phlsrng  16817  ocvss  16852  obsss  16906  fclsfil  17995  tmdtps  18059  tgptmd  18062  trgrng  18153  tdrgdrng  18156  ngpms  18600  icopnfcnv  18920  xrhmeo  18924  oprpiece1res2  18930  phtpcer  18973  pcoval2  18994  pcoass  19002  clmsca  19043  cphsqrcl  19100  bncms  19250  itg2ge0  19580  uc1pn0  20021  mon1pn0  20022  sinq12ge0  20369  cosq14gt0  20371  cosq14ge0  20372  sinord  20389  recosf1o  20390  resinf1o  20391  logrnaddcl  20425  atanf  20673  atanneg  20700  atancj  20703  efiatan  20705  atanlogaddlem  20706  atanlogadd  20707  atanlogsub  20709  efiatan2  20710  2efiatan  20711  tanatan  20712  dvatan  20728  areambl  20750  rlimcnp  20757  emgt0  20798  harmoniclbnd  20800  harmonicbnd4  20802  2sqlem2  21101  2sqlem3  21103  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  logdivbnd  21203  pntpbnd2  21234  pnt  21261  subgores  21845  subgoid  21848  subgoinv  21849  subgoablo  21852  ghsubgolem  21911  hst1a  23674  stge0  23680  sthil  23690  fsumrp0cl  24170  ofldtos  24190  elunitge0  24250  xrge0iifcnv  24272  xrge0iifcv  24273  xrge0iifiso  24274  logbcl  24350  voliune  24538  volfiniune  24539  lgamgulmlem2  24767  dfon2lem1  25353  dfrdg2  25366  brbtwn2  25748  ax5seglem3  25774  ax5seglem6  25777  axpaschlem  25783  axcontlem2  25808  axcontlem4  25810  locfinbas  26271  cntotbnd  26395  heiborlem5  26414  heiborlem6  26415  psgnunilem5  27285  stoweidlem60  27676  bnj563  28817  bnj1212  28877  bnj1219  28878  bnj1366  28907  bnj1379  28908  bnj545  28972  bnj594  28989  bnj1118  29059  bnj1177  29081  bnj1190  29083  bnj1398  29109  bnj1417  29116  bnj1450  29125  bnj1312  29133  bnj1523  29146  atl0cl  29786  dalem-ccly  30167
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