Theorem simp3bi 1165

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  limuni  6424  smores2  8347  ersym  8713  ertr  8716  fvixp  8913  undifixp  8945  fiint  9300  winalim2  10709  inar1  10788  supmullem1  12213  supmullem2  12214  supmul  12215  eluzle  12904  ico01fl0  13884  ef01bndlem  16278  sin01bnd  16279  cos01bnd  16280  sin01gt0  16284  divalglem6  16494  gznegcl  17033  gzcjcl  17034  gzaddcl  17035  gzmulcl  17036  gzabssqcl  17039  4sqlem4a  17049  prdsbasprj  17563  xpsff1o  17659  mreintcl  17685  drsdir  18396  subggrp  19258  pmtrfconj  19599  symggen  19603  psgnunilem1  19626  subgpgp  19730  slwispgp  19744  sylow2alem1  19750  oppglsm  19775  efgsdmi  19865  efgsrel  19867  efgsp1  19870  efgsres  19871  efgcpbllemb  19888  efgcpbl  19889  omndadd  20261  srgdilem  20337  srgrz  20352  srglz  20353  ringdilem  20394  isringrng  20434  dfring2  20435  ringsrg  20445  irredmul  20576  subrngss  20716  sdrgdrng  20962  fldsdrgfld  20970  sdrgint  20976  primefld  20977  orngmul  21037  lmodlema  21055  lsscl  21132  phllmhm  21851  ipcj  21853  ipeq0  21857  ocvi  21888  obsip  21940  obsocv  21945  2ndcctbss  23687  locfinnei  23755  fclssscls  24250  tmdcn  24315  tgpinv  24317  trgtmd  24397  tdrgunit  24399  ngpds  24836  nrmtngdist  24889  elii1  25169  elii2  25170  icopnfcnv  25176  icopnfhmeo  25177  iccpnfhmeo  25179  xrhmeo  25180  phtpcer  25229  pcoass  25258  clmsubrg  25300  cphnmfval  25426  bnsca  25573  uc1pldg  26381  mon1pldg  26382  sinq12ge0  26753  cosq14gt0  26755  cosq14ge0  26756  cos02pilt1  26771  cosq34lt1  26772  sinord  26779  recosf1o  26780  resinf1o  26781  logrnaddcl  26819  logimul  26859  dvlog2lem  26897  atanf  27125  atanneg  27152  atancj  27155  efiatan  27157  atanlogaddlem  27158  atanlogadd  27159  atanlogsub  27161  efiatan2  27162  2efiatan  27163  ressatans  27179  dvatan  27180  areaf  27206  harmonicubnd  27254  harmonicbnd4  27255  lgamgulmlem2  27274  2sqlem2  27662  2sqlem3  27664  dchrvmasumiflem1  27745  pntpbnd2  27831  f1otrg  29335  f1otrge  29336  brbtwn2  29370  ax5seglem3  29396  axpaschlem  29405  axcontlem7  29435  pthhashvtx  30202  hstel2  32708  stle1  32714  stj  32724  neldifpr2  33017  xrge0adddir  33466  slmdlema  33651  lmodslmd  33652  fldgensdrg  33763  rhmimaidl  33868  irngnzply1lem  34208  xrge0iifcnv  34451  xrge0iifiso  34453  xrge0iifhom  34455  rrextcusp  34523  rrextust  34526  unelros  34690  difelros  34691  inelsros  34697  diffiunisros  34698  sibfinima  34858  eulerpartlemf  34889  eulerpartlemgvv  34895  bnj563  35261  bnj1366  35346  bnj1379  35347  bnj554  35416  bnj557  35418  bnj570  35422  bnj594  35429  bnj1001  35476  bnj1006  35477  bnj1097  35498  bnj1177  35523  bnj1388  35550  bnj1398  35551  bnj1450  35567  bnj1501  35584  bnj1523  35588  snmlflim  35919  msrval  36125  mclsssvlem  36149  mclsind  36157  ptrecube  38377  cntotbnd  38554  heiborlem8  38576  dmnnzd  38833  eqvreltrrel  39440  atlex  40197  kelac1  43912  binomcxplemcvg  45186  binomcxplemnotnn0  45188  elixpconstg  45929  fvixp2  46038  stoweidlem39  46875  stoweidlem60  46896  fourierdlem40  46983  fourierdlem78  47020  idomnzd  49269  arweuthinc  50463