Theorem simp3bi 1148

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 215	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp3d 1145	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  limuni  6423  smores2  8351  ersym  8712  ertr  8715  fvixp  8893  undifixp  8925  fiint  9321  winalim2  10688  inar1  10767  supmullem1  12181  supmullem2  12182  supmul  12183  eluzle  12832  ico01fl0  13781  ef01bndlem  16124  sin01bnd  16125  cos01bnd  16126  sin01gt0  16130  divalglem6  16338  gznegcl  16865  gzcjcl  16866  gzaddcl  16867  gzmulcl  16868  gzabssqcl  16871  4sqlem4a  16881  prdsbasprj  17415  xpsff1o  17510  mreintcl  17536  drsdir  18252  subggrp  19004  pmtrfconj  19329  symggen  19333  psgnunilem1  19356  subgpgp  19460  slwispgp  19474  sylow2alem1  19480  oppglsm  19505  efgsdmi  19595  efgsrel  19597  efgsp1  19600  efgsres  19601  efgcpbllemb  19618  efgcpbl  19619  srgdilem  20009  srgrz  20024  srglz  20025  ringdilem  20066  ringsrg  20103  irredmul  20236  sdrgdrng  20399  fldsdrgfld  20407  sdrgint  20413  primefld  20414  lmodlema  20469  lsscl  20546  phllmhm  21177  ipcj  21179  ipeq0  21183  ocvi  21214  obsip  21268  obsocv  21273  2ndcctbss  22951  locfinnei  23019  fclssscls  23514  tmdcn  23579  tgpinv  23581  trgtmd  23661  tdrgunit  23663  ngpds  24105  nrmtngdist  24166  elii1  24443  elii2  24444  icopnfcnv  24450  icopnfhmeo  24451  iccpnfhmeo  24453  xrhmeo  24454  phtpcer  24503  pcoass  24532  clmsubrg  24574  cphnmfval  24701  bnsca  24848  uc1pldg  25658  mon1pldg  25659  sinq12ge0  26010  cosq14gt0  26012  cosq14ge0  26013  cos02pilt1  26027  cosq34lt1  26028  sinord  26035  recosf1o  26036  resinf1o  26037  logrnaddcl  26075  logimul  26114  dvlog2lem  26152  atanf  26375  atanneg  26402  atancj  26405  efiatan  26407  atanlogaddlem  26408  atanlogadd  26409  atanlogsub  26411  efiatan2  26412  2efiatan  26413  ressatans  26429  dvatan  26430  areaf  26456  harmonicubnd  26504  harmonicbnd4  26505  lgamgulmlem2  26524  2sqlem2  26911  2sqlem3  26913  dchrvmasumiflem1  26994  pntpbnd2  27080  f1otrg  28112  f1otrge  28113  brbtwn2  28153  ax5seglem3  28179  axpaschlem  28188  axcontlem7  28218  hstel2  31460  stle1  31466  stj  31476  neldifpr2  31759  xrge0adddir  32181  omndadd  32212  slmdlema  32336  lmodslmd  32337  fldgensdrg  32393  orngmul  32410  rhmimaidl  32539  irngnzply1lem  32743  xrge0iifcnv  32902  xrge0iifiso  32904  xrge0iifhom  32906  rrextcusp  32974  rrextust  32977  unelros  33158  difelros  33159  inelsros  33165  diffiunisros  33166  sibfinima  33327  eulerpartlemf  33358  eulerpartlemgvv  33364  bnj563  33743  bnj1366  33829  bnj1379  33830  bnj554  33899  bnj557  33901  bnj570  33905  bnj594  33912  bnj1001  33959  bnj1006  33960  bnj1097  33981  bnj1177  34006  bnj1388  34033  bnj1398  34034  bnj1450  34050  bnj1501  34067  bnj1523  34071  pthhashvtx  34107  snmlflim  34312  msrval  34518  mclsssvlem  34542  mclsind  34550  ptrecube  36477  cntotbnd  36653  heiborlem8  36675  dmnnzd  36932  eqvreltrrel  37459  atlex  38175  kelac1  41791  binomcxplemcvg  43099  binomcxplemnotnn0  43101  elixpconstg  43764  fvixp2  43884  stoweidlem39  44742  stoweidlem60  44763  fourierdlem40  44850  fourierdlem78  44887  isringrng  46644  subrngss  46712