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

Theorem simp1bi 1142
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 219 . 2 (𝜑 → (𝜓𝜒𝜃))
32simp1d 1139 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  limord  6237  smores2  7987  smofvon2  7989  smofvon  7992  errel  8294  elunitrn  12854  lincmb01cmp  12882  iccf1o  12883  elfznn0  13004  elfzouz  13046  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  sin01gt0  15543  cos01gt0  15544  sin02gt0  15545  gzcn  16266  mresspw  16863  drsprs  17546  ipodrscl  17772  subgrcl  18284  pmtrfconj  18594  pgpprm  18718  slwprm  18734  efgsdmi  18858  efgsrel  18860  efgs1b  18862  efgsp1  18863  efgsres  18864  efgsfo  18865  efgredlema  18866  efgredlemf  18867  efgredlemd  18870  efgredlemc  18871  efgredlem  18873  efgrelexlemb  18876  efgcpbllemb  18881  srgcmn  19258  ringgrp  19302  irredcl  19457  lmodgrp  19641  lssss  19708  phllvec  20773  obsrcl  20867  locfintop  22129  fclstop  22619  tmdmnd  22683  tgpgrp  22686  trgtgp  22776  tdrgtrg  22781  ust0  22828  ngpgrp  23208  elii1  23543  elii2  23544  icopnfcnv  23550  icopnfhmeo  23551  iccpnfhmeo  23553  xrhmeo  23554  oprpiece1res2  23560  phtpcer  23603  pcoval2  23624  pcoass  23632  clmlmod  23675  cphphl  23779  cphnlm  23780  cphsca  23787  bnnvc  23947  uc1pcl  24747  mon1pcl  24748  sinq12ge0  25104  cosq14ge0  25107  cosq34lt1  25122  cosord  25126  cos11  25128  recosf1o  25130  resinf1o  25131  efifo  25142  logrncn  25157  atanf  25469  atanneg  25496  efiatan  25501  atanlogaddlem  25502  atanlogadd  25503  atanlogsub  25505  efiatan2  25506  2efiatan  25507  tanatan  25508  areass  25548  dchrvmasumlem2  26085  dchrvmasumiflem1  26088  brbtwn2  26702  ax5seglem1  26725  ax5seglem2  26726  ax5seglem3  26728  ax5seglem5  26730  ax5seglem6  26731  ax5seglem9  26734  ax5seg  26735  axbtwnid  26736  axpaschlem  26737  axpasch  26738  axcontlem2  26762  axcontlem4  26764  axcontlem7  26767  pthistrl  27517  clwwlkbp  27773  sticl  30001  hstcl  30003  omndmnd  30737  slmdcmn  30865  orngring  30906  rrextnrg  31299  rrextdrg  31300  rossspw  31485  srossspw  31492  eulerpartlemd  31681  eulerpartlemf  31685  eulerpartlemgvv  31691  eulerpartlemgu  31692  eulerpartlemgh  31693  eulerpartlemgs2  31695  eulerpartlemn  31696  bnj564  32072  bnj1366  32158  bnj545  32224  bnj548  32226  bnj558  32231  bnj570  32234  bnj580  32242  bnj929  32265  bnj998  32286  bnj1006  32289  bnj1190  32337  bnj1523  32400  msrval  32842  mthmpps  32886  eqvrelrefrel  35938  atllat  36541  stoweidlem60  42628  fourierdlem111  42785  prproropf1o  43950  rngabl  44427
  Copyright terms: Public domain W3C validator