Theorem simp3bi 1146

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp3bi	⊢ (𝜑 → 𝜃)

Proof of Theorem simp3bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 216	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp3d 1143	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  limuni  6446  smores2  8392  ersym  8755  ertr  8758  fvixp  8940  undifixp  8972  fiint  9363  fiintOLD  9364  winalim2  10733  inar1  10812  supmullem1  12235  supmullem2  12236  supmul  12237  eluzle  12888  ico01fl0  13855  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  sin01gt0  16222  divalglem6  16431  gznegcl  16968  gzcjcl  16969  gzaddcl  16970  gzmulcl  16971  gzabssqcl  16974  4sqlem4a  16984  prdsbasprj  17518  xpsff1o  17613  mreintcl  17639  drsdir  18359  subggrp  19159  pmtrfconj  19498  symggen  19502  psgnunilem1  19525  subgpgp  19629  slwispgp  19643  sylow2alem1  19649  oppglsm  19674  efgsdmi  19764  efgsrel  19766  efgsp1  19769  efgsres  19770  efgcpbllemb  19787  efgcpbl  19788  srgdilem  20209  srgrz  20224  srglz  20225  ringdilem  20266  isringrng  20300  ringsrg  20310  irredmul  20445  subrngss  20564  sdrgdrng  20807  fldsdrgfld  20815  sdrgint  20821  primefld  20822  lmodlema  20879  lsscl  20957  phllmhm  21667  ipcj  21669  ipeq0  21673  ocvi  21704  obsip  21758  obsocv  21763  2ndcctbss  23478  locfinnei  23546  fclssscls  24041  tmdcn  24106  tgpinv  24108  trgtmd  24188  tdrgunit  24190  ngpds  24632  nrmtngdist  24693  elii1  24977  elii2  24978  icopnfcnv  24986  icopnfhmeo  24987  iccpnfhmeo  24989  xrhmeo  24990  phtpcer  25040  pcoass  25070  clmsubrg  25112  cphnmfval  25239  bnsca  25386  uc1pldg  26202  mon1pldg  26203  sinq12ge0  26564  cosq14gt0  26566  cosq14ge0  26567  cos02pilt1  26582  cosq34lt1  26583  sinord  26590  recosf1o  26591  resinf1o  26592  logrnaddcl  26630  logimul  26670  dvlog2lem  26708  atanf  26937  atanneg  26964  atancj  26967  efiatan  26969  atanlogaddlem  26970  atanlogadd  26971  atanlogsub  26973  efiatan2  26974  2efiatan  26975  ressatans  26991  dvatan  26992  areaf  27018  harmonicubnd  27067  harmonicbnd4  27068  lgamgulmlem2  27087  2sqlem2  27476  2sqlem3  27478  dchrvmasumiflem1  27559  pntpbnd2  27645  f1otrg  28893  f1otrge  28894  brbtwn2  28934  ax5seglem3  28960  axpaschlem  28969  axcontlem7  28999  hstel2  32247  stle1  32253  stj  32263  neldifpr2  32559  xrge0adddir  33005  omndadd  33065  slmdlema  33191  lmodslmd  33192  fldgensdrg  33295  orngmul  33312  rhmimaidl  33439  irngnzply1lem  33704  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhom  33897  rrextcusp  33967  rrextust  33970  unelros  34151  difelros  34152  inelsros  34158  diffiunisros  34159  sibfinima  34320  eulerpartlemf  34351  eulerpartlemgvv  34357  bnj563  34735  bnj1366  34821  bnj1379  34822  bnj554  34891  bnj557  34893  bnj570  34897  bnj594  34904  bnj1001  34951  bnj1006  34952  bnj1097  34973  bnj1177  34998  bnj1388  35025  bnj1398  35026  bnj1450  35042  bnj1501  35059  bnj1523  35063  pthhashvtx  35111  snmlflim  35316  msrval  35522  mclsssvlem  35546  mclsind  35554  ptrecube  37606  cntotbnd  37782  heiborlem8  37804  dmnnzd  38061  eqvreltrrel  38581  atlex  39297  kelac1  43051  binomcxplemcvg  44349  binomcxplemnotnn0  44351  elixpconstg  45028  fvixp2  45141  stoweidlem39  45994  stoweidlem60  46015  fourierdlem40  46102  fourierdlem78  46139