Theorem simp3bi 1145

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

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

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 395  df-3an 1087

This theorem is referenced by:  limuni  6424  smores2  8356  ersym  8717  ertr  8720  fvixp  8898  undifixp  8930  fiint  9326  winalim2  10693  inar1  10772  supmullem1  12188  supmullem2  12189  supmul  12190  eluzle  12839  ico01fl0  13788  ef01bndlem  16131  sin01bnd  16132  cos01bnd  16133  sin01gt0  16137  divalglem6  16345  gznegcl  16872  gzcjcl  16873  gzaddcl  16874  gzmulcl  16875  gzabssqcl  16878  4sqlem4a  16888  prdsbasprj  17422  xpsff1o  17517  mreintcl  17543  drsdir  18259  subggrp  19045  pmtrfconj  19375  symggen  19379  psgnunilem1  19402  subgpgp  19506  slwispgp  19520  sylow2alem1  19526  oppglsm  19551  efgsdmi  19641  efgsrel  19643  efgsp1  19646  efgsres  19647  efgcpbllemb  19664  efgcpbl  19665  srgdilem  20086  srgrz  20101  srglz  20102  ringdilem  20143  isringrng  20175  ringsrg  20185  irredmul  20320  subrngss  20436  sdrgdrng  20549  fldsdrgfld  20557  sdrgint  20563  primefld  20564  lmodlema  20619  lsscl  20697  phllmhm  21404  ipcj  21406  ipeq0  21410  ocvi  21441  obsip  21495  obsocv  21500  2ndcctbss  23179  locfinnei  23247  fclssscls  23742  tmdcn  23807  tgpinv  23809  trgtmd  23889  tdrgunit  23891  ngpds  24333  nrmtngdist  24394  elii1  24678  elii2  24679  icopnfcnv  24687  icopnfhmeo  24688  iccpnfhmeo  24690  xrhmeo  24691  phtpcer  24741  pcoass  24771  clmsubrg  24813  cphnmfval  24940  bnsca  25087  uc1pldg  25901  mon1pldg  25902  sinq12ge0  26254  cosq14gt0  26256  cosq14ge0  26257  cos02pilt1  26271  cosq34lt1  26272  sinord  26279  recosf1o  26280  resinf1o  26281  logrnaddcl  26319  logimul  26358  dvlog2lem  26396  atanf  26621  atanneg  26648  atancj  26651  efiatan  26653  atanlogaddlem  26654  atanlogadd  26655  atanlogsub  26657  efiatan2  26658  2efiatan  26659  ressatans  26675  dvatan  26676  areaf  26702  harmonicubnd  26750  harmonicbnd4  26751  lgamgulmlem2  26770  2sqlem2  27157  2sqlem3  27159  dchrvmasumiflem1  27240  pntpbnd2  27326  f1otrg  28389  f1otrge  28390  brbtwn2  28430  ax5seglem3  28456  axpaschlem  28465  axcontlem7  28495  hstel2  31739  stle1  31745  stj  31755  neldifpr2  32038  xrge0adddir  32460  omndadd  32494  slmdlema  32618  lmodslmd  32619  fldgensdrg  32674  orngmul  32691  rhmimaidl  32824  irngnzply1lem  33043  xrge0iifcnv  33211  xrge0iifiso  33213  xrge0iifhom  33215  rrextcusp  33283  rrextust  33286  unelros  33467  difelros  33468  inelsros  33474  diffiunisros  33475  sibfinima  33636  eulerpartlemf  33667  eulerpartlemgvv  33673  bnj563  34052  bnj1366  34138  bnj1379  34139  bnj554  34208  bnj557  34210  bnj570  34214  bnj594  34221  bnj1001  34268  bnj1006  34269  bnj1097  34290  bnj1177  34315  bnj1388  34342  bnj1398  34343  bnj1450  34359  bnj1501  34376  bnj1523  34380  pthhashvtx  34416  snmlflim  34621  msrval  34827  mclsssvlem  34851  mclsind  34859  ptrecube  36791  cntotbnd  36967  heiborlem8  36989  dmnnzd  37246  eqvreltrrel  37773  atlex  38489  kelac1  42107  binomcxplemcvg  43415  binomcxplemnotnn0  43417  elixpconstg  44079  fvixp2  44196  stoweidlem39  45053  stoweidlem60  45074  fourierdlem40  45161  fourierdlem78  45198