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

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

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 1105

This theorem is referenced by:  limuni  6425  smores2  8342  ersym  8708  ertr  8711  fvixp  8901  undifixp  8933  fiint  9287  winalim2  10682  inar1  10761  supmullem1  12186  supmullem2  12187  supmul  12188  eluzle  12876  ico01fl0  13854  ef01bndlem  16241  sin01bnd  16242  cos01bnd  16243  sin01gt0  16247  divalglem6  16457  gznegcl  16996  gzcjcl  16997  gzaddcl  16998  gzmulcl  16999  gzabssqcl  17002  4sqlem4a  17012  prdsbasprj  17526  xpsff1o  17622  mreintcl  17648  drsdir  18359  subggrp  19196  pmtrfconj  19537  symggen  19541  psgnunilem1  19564  subgpgp  19668  slwispgp  19682  sylow2alem1  19688  oppglsm  19713  efgsdmi  19803  efgsrel  19805  efgsp1  19808  efgsres  19809  efgcpbllemb  19826  efgcpbl  19827  omndadd  20199  srgdilem  20275  srgrz  20290  srglz  20291  ringdilem  20332  isringrng  20371  ringsrg  20381  irredmul  20512  subrngss  20634  sdrgdrng  20874  fldsdrgfld  20882  sdrgint  20888  primefld  20889  orngmul  20949  lmodlema  20967  lsscl  21044  phllmhm  21763  ipcj  21765  ipeq0  21769  ocvi  21800  obsip  21852  obsocv  21857  2ndcctbss  23593  locfinnei  23661  fclssscls  24156  tmdcn  24221  tgpinv  24223  trgtmd  24303  tdrgunit  24305  ngpds  24742  nrmtngdist  24795  elii1  25075  elii2  25076  icopnfcnv  25082  icopnfhmeo  25083  iccpnfhmeo  25085  xrhmeo  25086  phtpcer  25135  pcoass  25164  clmsubrg  25206  cphnmfval  25332  bnsca  25479  uc1pldg  26287  mon1pldg  26288  sinq12ge0  26654  cosq14gt0  26656  cosq14ge0  26657  cos02pilt1  26672  cosq34lt1  26673  sinord  26680  recosf1o  26681  resinf1o  26682  logrnaddcl  26720  logimul  26760  dvlog2lem  26798  atanf  27026  atanneg  27053  atancj  27056  efiatan  27058  atanlogaddlem  27059  atanlogadd  27060  atanlogsub  27062  efiatan2  27063  2efiatan  27064  ressatans  27080  dvatan  27081  areaf  27107  harmonicubnd  27155  harmonicbnd4  27156  lgamgulmlem2  27175  2sqlem2  27563  2sqlem3  27565  dchrvmasumiflem1  27646  pntpbnd2  27732  f1otrg  29201  f1otrge  29202  brbtwn2  29236  ax5seglem3  29262  axpaschlem  29271  axcontlem7  29301  hstel2  32552  stle1  32558  stj  32568  neldifpr2  32861  xrge0adddir  33319  slmdlema  33504  lmodslmd  33505  fldgensdrg  33616  rhmimaidl  33721  irngnzply1lem  34061  xrge0iifcnv  34304  xrge0iifiso  34306  xrge0iifhom  34308  rrextcusp  34376  rrextust  34379  unelros  34542  difelros  34543  inelsros  34549  diffiunisros  34550  sibfinima  34710  eulerpartlemf  34741  eulerpartlemgvv  34747  bnj563  35113  bnj1366  35198  bnj1379  35199  bnj554  35268  bnj557  35270  bnj570  35274  bnj594  35281  bnj1001  35328  bnj1006  35329  bnj1097  35350  bnj1177  35375  bnj1388  35402  bnj1398  35403  bnj1450  35419  bnj1501  35436  bnj1523  35440  pthhashvtx  35601  snmlflim  35805  msrval  36011  mclsssvlem  36035  mclsind  36043  ptrecube  38252  cntotbnd  38428  heiborlem8  38450  dmnnzd  38707  eqvreltrrel  39314  atlex  40071  kelac1  43773  binomcxplemcvg  45047  binomcxplemnotnn0  45049  elixpconstg  45790  fvixp2  45899  stoweidlem39  46736  stoweidlem60  46757  fourierdlem40  46844  fourierdlem78  46881  idomnzd  49094  arweuthinc  50290