Theorem simp3bi 1163

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 1160	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  limuni  6412  smores2  8329  ersym  8695  ertr  8698  fvixp  8888  undifixp  8920  fiint  9274  winalim2  10669  inar1  10748  supmullem1  12176  supmullem2  12177  supmul  12178  eluzle  12866  ico01fl0  13843  ef01bndlem  16230  sin01bnd  16231  cos01bnd  16232  sin01gt0  16236  divalglem6  16446  gznegcl  16985  gzcjcl  16986  gzaddcl  16987  gzmulcl  16988  gzabssqcl  16991  4sqlem4a  17001  prdsbasprj  17515  xpsff1o  17611  mreintcl  17637  drsdir  18348  subggrp  19186  pmtrfconj  19527  symggen  19531  psgnunilem1  19554  subgpgp  19658  slwispgp  19672  sylow2alem1  19678  oppglsm  19703  efgsdmi  19793  efgsrel  19795  efgsp1  19798  efgsres  19799  efgcpbllemb  19816  efgcpbl  19817  omndadd  20189  srgdilem  20265  srgrz  20280  srglz  20281  ringdilem  20322  isringrng  20361  ringsrg  20371  irredmul  20502  subrngss  20624  sdrgdrng  20862  fldsdrgfld  20870  sdrgint  20876  primefld  20877  orngmul  20937  lmodlema  20955  lsscl  21032  phllmhm  21742  ipcj  21744  ipeq0  21748  ocvi  21779  obsip  21831  obsocv  21836  2ndcctbss  23573  locfinnei  23641  fclssscls  24136  tmdcn  24201  tgpinv  24203  trgtmd  24283  tdrgunit  24285  ngpds  24722  nrmtngdist  24775  elii1  25055  elii2  25056  icopnfcnv  25062  icopnfhmeo  25063  iccpnfhmeo  25065  xrhmeo  25066  phtpcer  25115  pcoass  25144  clmsubrg  25186  cphnmfval  25312  bnsca  25459  uc1pldg  26267  mon1pldg  26268  sinq12ge0  26631  cosq14gt0  26633  cosq14ge0  26634  cos02pilt1  26649  cosq34lt1  26650  sinord  26657  recosf1o  26658  resinf1o  26659  logrnaddcl  26697  logimul  26737  dvlog2lem  26775  atanf  27003  atanneg  27030  atancj  27033  efiatan  27035  atanlogaddlem  27036  atanlogadd  27037  atanlogsub  27039  efiatan2  27040  2efiatan  27041  ressatans  27057  dvatan  27058  areaf  27084  harmonicubnd  27132  harmonicbnd4  27133  lgamgulmlem2  27152  2sqlem2  27540  2sqlem3  27542  dchrvmasumiflem1  27623  pntpbnd2  27709  f1otrg  29129  f1otrge  29130  brbtwn2  29164  ax5seglem3  29190  axpaschlem  29199  axcontlem7  29229  hstel2  32480  stle1  32486  stj  32496  neldifpr2  32790  xrge0adddir  33251  slmdlema  33436  lmodslmd  33437  fldgensdrg  33550  rhmimaidl  33656  irngnzply1lem  33997  xrge0iifcnv  34240  xrge0iifiso  34242  xrge0iifhom  34244  rrextcusp  34312  rrextust  34315  unelros  34478  difelros  34479  inelsros  34485  diffiunisros  34486  sibfinima  34646  eulerpartlemf  34677  eulerpartlemgvv  34683  bnj563  35049  bnj1366  35134  bnj1379  35135  bnj554  35204  bnj557  35206  bnj570  35210  bnj594  35217  bnj1001  35264  bnj1006  35265  bnj1097  35286  bnj1177  35311  bnj1388  35338  bnj1398  35339  bnj1450  35355  bnj1501  35372  bnj1523  35376  pthhashvtx  35491  snmlflim  35695  msrval  35901  mclsssvlem  35925  mclsind  35933  ptrecube  38131  cntotbnd  38307  heiborlem8  38329  dmnnzd  38586  eqvreltrrel  39195  atlex  39952  kelac1  43652  binomcxplemcvg  44928  binomcxplemnotnn0  44930  elixpconstg  45665  fvixp2  45774  stoweidlem39  46611  stoweidlem60  46632  fourierdlem40  46719  fourierdlem78  46756  arweuthinc  50158