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

Theorem simp1bi 1168
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 207 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp1d 1165 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  limord  5994  smores2  7684  smofvon2  7686  smofvon  7689  errel  7985  lincmb01cmp  12534  iccf1o  12535  elfznn0  12652  elfzouz  12694  ef01bndlem  15130  sin01bnd  15131  cos01bnd  15132  sin01gt0  15136  cos01gt0  15137  sin02gt0  15138  gzcn  15849  mresspw  16453  drsprs  17137  ipodrscl  17363  subgrcl  17797  pmtrfconj  18083  pgpprm  18205  slwprm  18221  efgsdmi  18342  efgsrel  18344  efgs1b  18346  efgsp1  18347  efgsres  18348  efgsfo  18349  efgredlema  18350  efgredlemf  18351  efgredlemd  18354  efgredlemc  18355  efgredlem  18357  efgrelexlemb  18360  efgcpbllemb  18365  srgcmn  18706  ringgrp  18750  irredcl  18902  lmodgrp  19070  lssss  19137  phllvec  20180  obsrcl  20273  locfintop  21534  fclstop  22024  tmdmnd  22088  tgpgrp  22091  trgtgp  22180  tdrgtrg  22185  ust0  22232  ngpgrp  22612  elii1  22943  elii2  22944  icopnfcnv  22950  icopnfhmeo  22951  iccpnfhmeo  22953  xrhmeo  22954  oprpiece1res1  22959  oprpiece1res2  22960  phtpcer  23003  pcoval2  23024  pcoass  23032  clmlmod  23075  cphphl  23179  cphnlm  23180  cphsca  23187  bnnvc  23345  uc1pcl  24113  mon1pcl  24114  sinq12ge0  24471  cosq14ge0  24474  cosord  24489  cos11  24490  recosf1o  24492  resinf1o  24493  efifo  24504  logrncn  24519  atanf  24817  atanneg  24844  efiatan  24849  atanlogaddlem  24850  atanlogadd  24851  atanlogsub  24853  efiatan2  24854  2efiatan  24855  tanatan  24856  areass  24896  dchrvmasumlem2  25397  dchrvmasumiflem1  25400  brbtwn2  25995  ax5seglem1  26018  ax5seglem2  26019  ax5seglem3  26021  ax5seglem5  26023  ax5seglem6  26024  ax5seglem9  26027  ax5seg  26028  axbtwnid  26029  axpaschlem  26030  axpasch  26031  axcontlem2  26055  axcontlem4  26057  axcontlem7  26060  pthistrl  26845  clwwlkbp  27124  sticl  29399  hstcl  29401  omndmnd  30026  slmdcmn  30080  orngring  30122  elunitrn  30265  rrextnrg  30367  rrextdrg  30368  rossspw  30554  srossspw  30561  eulerpartlemd  30750  eulerpartlemf  30754  eulerpartlemgvv  30760  eulerpartlemgu  30761  eulerpartlemgh  30762  eulerpartlemgs2  30764  eulerpartlemn  30765  bnj564  31134  bnj1366  31220  bnj545  31285  bnj548  31287  bnj558  31292  bnj570  31295  bnj580  31303  bnj929  31326  bnj998  31346  bnj1006  31349  bnj1190  31396  bnj1523  31459  msrval  31755  mthmpps  31799  atllat  35077  stoweidlem60  40753  fourierdlem111  40910  rngabl  42442
  Copyright terms: Public domain W3C validator