Theorem simp3bi 1159

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  limuni  6404  smores2  8320  ersym  8686  ertr  8689  fvixp  8880  undifixp  8912  fiint  9267  winalim2  10651  inar1  10730  supmullem1  12159  supmullem2  12160  supmul  12161  eluzle  12849  ico01fl0  13826  ef01bndlem  16199  sin01bnd  16200  cos01bnd  16201  sin01gt0  16205  divalglem6  16415  gznegcl  16954  gzcjcl  16955  gzaddcl  16956  gzmulcl  16957  gzabssqcl  16960  4sqlem4a  16970  prdsbasprj  17484  xpsff1o  17580  mreintcl  17606  drsdir  18317  subggrp  19154  pmtrfconj  19489  symggen  19493  psgnunilem1  19516  subgpgp  19620  slwispgp  19634  sylow2alem1  19640  oppglsm  19665  efgsdmi  19755  efgsrel  19757  efgsp1  19760  efgsres  19761  efgcpbllemb  19778  efgcpbl  19779  omndadd  20151  srgdilem  20221  srgrz  20236  srglz  20237  ringdilem  20278  isringrng  20316  ringsrg  20326  irredmul  20457  subrngss  20577  sdrgdrng  20819  fldsdrgfld  20827  sdrgint  20833  primefld  20834  orngmul  20894  lmodlema  20912  lsscl  20989  phllmhm  21664  ipcj  21666  ipeq0  21670  ocvi  21701  obsip  21753  obsocv  21758  2ndcctbss  23495  locfinnei  23563  fclssscls  24058  tmdcn  24123  tgpinv  24125  trgtmd  24205  tdrgunit  24207  ngpds  24644  nrmtngdist  24697  elii1  24977  elii2  24978  icopnfcnv  24984  icopnfhmeo  24985  iccpnfhmeo  24987  xrhmeo  24988  phtpcer  25037  pcoass  25066  clmsubrg  25108  cphnmfval  25234  bnsca  25381  uc1pldg  26189  mon1pldg  26190  sinq12ge0  26550  cosq14gt0  26552  cosq14ge0  26553  cos02pilt1  26568  cosq34lt1  26569  sinord  26576  recosf1o  26577  resinf1o  26578  logrnaddcl  26616  logimul  26656  dvlog2lem  26694  atanf  26922  atanneg  26949  atancj  26952  efiatan  26954  atanlogaddlem  26955  atanlogadd  26956  atanlogsub  26958  efiatan2  26959  2efiatan  26960  ressatans  26976  dvatan  26977  areaf  27003  harmonicubnd  27051  harmonicbnd4  27052  lgamgulmlem2  27071  2sqlem2  27459  2sqlem3  27461  dchrvmasumiflem1  27542  pntpbnd2  27628  f1otrg  29017  f1otrge  29018  brbtwn2  29052  ax5seglem3  29078  axpaschlem  29087  axcontlem7  29117  hstel2  32368  stle1  32374  stj  32384  neldifpr2  32682  xrge0adddir  33157  slmdlema  33344  lmodslmd  33345  fldgensdrg  33462  rhmimaidl  33579  irngnzply1lem  33948  xrge0iifcnv  34191  xrge0iifiso  34193  xrge0iifhom  34195  rrextcusp  34263  rrextust  34266  unelros  34429  difelros  34430  inelsros  34436  diffiunisros  34437  sibfinima  34597  eulerpartlemf  34628  eulerpartlemgvv  34634  bnj563  35003  bnj1366  35088  bnj1379  35089  bnj554  35158  bnj557  35160  bnj570  35164  bnj594  35171  bnj1001  35218  bnj1006  35219  bnj1097  35240  bnj1177  35265  bnj1388  35292  bnj1398  35293  bnj1450  35309  bnj1501  35326  bnj1523  35330  pthhashvtx  35442  snmlflim  35646  msrval  35852  mclsssvlem  35876  mclsind  35884  ptrecube  38083  cntotbnd  38259  heiborlem8  38281  dmnnzd  38538  eqvreltrrel  39147  atlex  39904  kelac1  43604  binomcxplemcvg  44894  binomcxplemnotnn0  44896  elixpconstg  45631  fvixp2  45740  stoweidlem39  46577  stoweidlem60  46598  fourierdlem40  46685  fourierdlem78  46722  arweuthinc  50114