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

Theorem simp3bi 1005
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 1002 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 965
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 967
This theorem is referenced by:  limuni  4800  smores2  6836  ersym  7134  ertr  7137  fvixp  7289  undifixp  7320  fiint  7609  winalim2  8884  inar1  8963  supmullem1  10317  supmullem2  10318  supmul  10319  eluzle  10894  ef01bndlem  13489  sin01bnd  13490  cos01bnd  13491  sin01gt0  13495  divalglem6  13623  gznegcl  14017  gzcjcl  14018  gzaddcl  14019  gzmulcl  14020  gzabssqcl  14023  4sqlem4a  14033  prdsbasprj  14431  xpsff1o  14527  mreintcl  14554  drsdir  15126  subggrp  15705  pmtrfconj  15993  symggen  15997  psgnunilem1  16020  subgpgp  16117  slwispgp  16131  sylow2alem1  16137  oppglsm  16162  efgsdmi  16250  efgsrel  16252  efgsp1  16255  efgsres  16256  efgcpbllemb  16273  efgcpbl  16274  srgi  16635  srgrz  16649  srglz  16650  rngi  16679  irredmul  16823  lmodlema  16975  lsscl  17046  phllmhm  18083  ipcj  18085  ipeq0  18089  ocvi  18116  obsip  18168  obsocv  18173  2ndcctbss  19081  fclssscls  19613  tmdcn  19676  tgpinv  19678  trgtmd  19761  tdrgunit  19763  ngpds  20217  elii1  20529  elii2  20530  icopnfcnv  20536  icopnfhmeo  20537  iccpnfhmeo  20539  xrhmeo  20540  phtpcer  20589  pcoass  20618  clmsubrg  20660  cphnmfval  20733  bnsca  20872  uc1pldg  21642  mon1pldg  21643  sinq12ge0  21992  cosq14gt0  21994  cosq14ge0  21995  sinord  22012  recosf1o  22013  resinf1o  22014  logrnaddcl  22048  logimul  22085  dvlog2lem  22119  atanf  22297  atanneg  22324  atancj  22327  efiatan  22329  atanlogaddlem  22330  atanlogadd  22331  atanlogsub  22333  efiatan2  22334  2efiatan  22335  ressatans  22351  dvatan  22352  areaf  22377  harmonicubnd  22425  harmonicbnd4  22426  2sqlem2  22725  2sqlem3  22727  dchrvmasumiflem1  22772  pntpbnd2  22858  f1otrg  23139  f1otrge  23140  brbtwn2  23173  ax5seglem3  23199  axpaschlem  23208  axcontlem7  23238  subgores  23813  hstel2  25645  stle1  25651  stj  25661  xrge0adddir  26177  omndadd  26191  slmdlema  26241  lmodslmd  26242  orngmul  26293  xrge0iifcnv  26385  xrge0iifiso  26387  xrge0iifhom  26389  rrextcusp  26456  rrextust  26459  sibfinima  26747  eulerpartlemf  26775  eulerpartlemgvv  26781  lgamgulmlem2  27038  snmlflim  27243  locfinnei  28600  cntotbnd  28721  heiborlem8  28743  dmnnzd  28901  kelac1  29442  stoweidlem39  29860  stoweidlem60  29881  bnj563  31831  bnj1366  31919  bnj1379  31920  bnj554  31988  bnj557  31990  bnj570  31994  bnj594  32001  bnj1001  32047  bnj1006  32048  bnj1097  32068  bnj1177  32093  bnj1388  32120  bnj1398  32121  bnj1450  32137  bnj1501  32154  bnj1523  32158  bj-flbi3  32623  atlex  33057
  Copyright terms: Public domain W3C validator