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

Theorem simp1bi 1074
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 206 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp1d 1071 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  limord  5748  smores2  7403  smofvon2  7405  smofvon  7408  errel  7703  lincmb01cmp  12264  iccf1o  12265  elfznn0  12381  elfzouz  12422  ef01bndlem  14846  sin01bnd  14847  cos01bnd  14848  sin01gt0  14852  cos01gt0  14853  sin02gt0  14854  gzcn  15567  mresspw  16180  drsprs  16864  ipodrscl  17090  subgrcl  17527  pmtrfconj  17814  pgpprm  17936  slwprm  17952  efgsdmi  18073  efgsrel  18075  efgs1b  18077  efgsp1  18078  efgsres  18079  efgsfo  18080  efgredlema  18081  efgredlemf  18082  efgredlemd  18085  efgredlemc  18086  efgredlem  18088  efgrelexlemb  18091  efgcpbllemb  18096  srgcmn  18436  ringgrp  18480  irredcl  18632  lmodgrp  18798  lssss  18865  phllvec  19902  obsrcl  19995  locfintop  21243  fclstop  21734  tmdmnd  21798  tgpgrp  21801  trgtgp  21890  tdrgtrg  21895  ust0  21942  ngpgrp  22322  elii1  22653  elii2  22654  icopnfcnv  22660  icopnfhmeo  22661  iccpnfhmeo  22663  xrhmeo  22664  oprpiece1res1  22669  oprpiece1res2  22670  phtpcer  22713  phtpcerOLD  22714  pcoval2  22735  pcoass  22743  clmlmod  22786  cphphl  22890  cphnlm  22891  cphsca  22898  bnnvc  23056  uc1pcl  23820  mon1pcl  23821  sinq12ge0  24177  cosq14ge0  24180  cosord  24195  cos11  24196  recosf1o  24198  resinf1o  24199  efifo  24210  logrncn  24226  atanf  24520  atanneg  24547  efiatan  24552  atanlogaddlem  24553  atanlogadd  24554  atanlogsub  24556  efiatan2  24557  2efiatan  24558  tanatan  24559  areass  24599  dchrvmasumlem2  25100  dchrvmasumiflem1  25103  brbtwn2  25698  ax5seglem1  25721  ax5seglem2  25722  ax5seglem3  25724  ax5seglem5  25726  ax5seglem6  25727  ax5seglem9  25730  ax5seg  25731  axbtwnid  25732  axpaschlem  25733  axpasch  25734  axcontlem2  25758  axcontlem4  25760  axcontlem7  25763  pthistrl  26503  clwwlkbp  26763  sticl  28941  hstcl  28943  omndmnd  29507  slmdcmn  29561  orngring  29603  elunitrn  29743  rrextnrg  29845  rrextdrg  29846  rossspw  30031  srossspw  30038  eulerpartlemd  30227  eulerpartlemf  30231  eulerpartlemgvv  30237  eulerpartlemgu  30238  eulerpartlemgh  30239  eulerpartlemgs2  30241  eulerpartlemn  30242  bnj564  30549  bnj1366  30635  bnj545  30700  bnj548  30702  bnj558  30707  bnj570  30710  bnj580  30718  bnj929  30741  bnj998  30761  bnj1006  30764  bnj1190  30811  bnj1523  30874  msrval  31170  mthmpps  31214  atllat  34094  stoweidlem60  39605  fourierdlem111  39762  rngabl  41186
  Copyright terms: Public domain W3C validator