MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1bi Structured version   Visualization version   GIF version

Theorem simp1bi 1145
Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
3simp1bi.1 (𝜑 ↔ (𝜓𝜒𝜃))
Assertion
Ref Expression
simp1bi (𝜑𝜓)

Proof of Theorem simp1bi
StepHypRef Expression
1 3simp1bi.1 . . 3 (𝜑 ↔ (𝜓𝜒𝜃))
21biimpi 215 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp1d 1142 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  limord  6375  smores2  8292  smofvon2  8294  smofvon  8297  errel  8615  elunitrn  13338  lincmb01cmp  13366  iccf1o  13367  elfznn0  13488  elfzouz  13530  ef01bndlem  16026  sin01bnd  16027  cos01bnd  16028  sin01gt0  16032  cos01gt0  16033  sin02gt0  16034  gzcn  16764  mresspw  17432  drsprs  18152  ipodrscl  18387  subgrcl  18892  pmtrfconj  19207  pgpprm  19334  slwprm  19350  efgsdmi  19473  efgsrel  19475  efgs1b  19477  efgsp1  19478  efgsres  19479  efgsfo  19480  efgredlema  19481  efgredlemf  19482  efgredlemd  19485  efgredlemc  19486  efgredlem  19488  efgrelexlemb  19491  efgcpbllemb  19496  srgcmn  19879  ringgrp  19923  irredcl  20086  lmodgrp  20282  lssss  20350  phllvec  20986  obsrcl  21082  locfintop  22824  fclstop  23314  tmdmnd  23378  tgpgrp  23381  trgtgp  23471  tdrgtrg  23476  ust0  23523  ngpgrp  23907  elii1  24250  elii2  24251  icopnfcnv  24257  icopnfhmeo  24258  iccpnfhmeo  24260  xrhmeo  24261  oprpiece1res2  24267  phtpcer  24310  pcoval2  24331  pcoass  24339  clmlmod  24382  cphphl  24487  cphnlm  24488  cphsca  24495  bnnvc  24656  uc1pcl  25460  mon1pcl  25461  sinq12ge0  25817  cosq14ge0  25820  cosq34lt1  25835  cosord  25839  cos11  25841  recosf1o  25843  resinf1o  25844  efifo  25855  logrncn  25870  atanf  26182  atanneg  26209  efiatan  26214  atanlogaddlem  26215  atanlogadd  26216  atanlogsub  26218  efiatan2  26219  2efiatan  26220  tanatan  26221  areass  26261  dchrvmasumlem2  26798  dchrvmasumiflem1  26801  brbtwn2  27683  ax5seglem1  27706  ax5seglem2  27707  ax5seglem3  27709  ax5seglem5  27711  ax5seglem6  27712  ax5seglem9  27715  ax5seg  27716  axbtwnid  27717  axpaschlem  27718  axpasch  27719  axcontlem2  27743  axcontlem4  27745  axcontlem7  27748  pthistrl  28502  clwwlkbp  28758  sticl  30986  hstcl  30988  omndmnd  31738  slmdcmn  31866  orngring  31921  rrextnrg  32394  rrextdrg  32395  rossspw  32580  srossspw  32587  eulerpartlemd  32778  eulerpartlemf  32782  eulerpartlemgvv  32788  eulerpartlemgu  32789  eulerpartlemgh  32790  eulerpartlemgs2  32792  eulerpartlemn  32793  bnj564  33168  bnj1366  33253  bnj545  33319  bnj548  33321  bnj558  33326  bnj570  33329  bnj580  33337  bnj929  33360  bnj998  33381  bnj1006  33384  bnj1190  33432  bnj1523  33495  msrval  33944  mthmpps  33988  eqvrelrefrel  36998  atllat  37700  stoweidlem60  44202  fourierdlem111  44359  prproropf1o  45600  rngabl  46076
  Copyright terms: Public domain W3C validator