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  6446  smores2  8393  ersym  8761  ertr  8764  fvixp  8961  undifixp  8993  fiint  9349  winalim2  10811  inar1  10890  supmullem1  12317  supmullem2  12318  supmul  12319  eluzle  13008  ico01fl0  13989  ef01bndlem  16384  sin01bnd  16385  cos01bnd  16386  sin01gt0  16390  divalglem6  16600  gznegcl  17145  gzcjcl  17146  gzaddcl  17147  gzmulcl  17148  gzabssqcl  17151  4sqlem4a  17161  prdsbasprj  17675  xpsff1o  17771  mreintcl  17797  drsdir  18508  subggrp  19371  pmtrfconj  19713  symggen  19717  psgnunilem1  19740  subgpgp  19844  slwispgp  19858  sylow2alem1  19864  oppglsm  19889  efgsdmi  19979  efgsrel  19981  efgsp1  19984  efgsres  19985  efgcpbllemb  20002  efgcpbl  20003  omndadd  20375  srgdilem  20451  srgrz  20466  srglz  20467  ringdilem  20509  isringrng  20549  dfring2  20550  ringsrg  20561  irredmul  20692  subrngss  20833  sdrgdrng  21080  fldsdrgfld  21088  sdrgint  21094  primefld  21095  orngmul  21155  lmodlema  21173  lsscl  21250  phllmhm  21971  ipcj  21973  ipeq0  21977  ocvi  22008  obsip  22060  obsocv  22065  2ndcctbss  23807  locfinnei  23875  fclssscls  24370  tmdcn  24435  tgpinv  24437  trgtmd  24517  tdrgunit  24519  ngpds  24956  nrmtngdist  25009  elii1  25289  elii2  25290  icopnfcnv  25296  icopnfhmeo  25297  iccpnfhmeo  25299  xrhmeo  25300  phtpcer  25349  pcoass  25378  clmsubrg  25420  cphnmfval  25546  bnsca  25693  uc1pldg  26500  mon1pldg  26501  sinq12ge0  26870  cosq14gt0  26872  cosq14ge0  26873  cos02pilt1  26887  cosq34lt1  26888  sinord  26895  recosf1o  26896  resinf1o  26897  logrnaddcl  26935  logimul  26975  dvlog2lem  27013  atanf  27241  atanneg  27268  atancj  27271  efiatan  27273  atanlogaddlem  27274  atanlogadd  27275  atanlogsub  27277  efiatan2  27278  2efiatan  27279  ressatans  27295  dvatan  27296  areaf  27322  harmonicubnd  27370  harmonicbnd4  27371  lgamgulmlem2  27390  2sqlem2  27778  2sqlem3  27780  dchrvmasumiflem1  27861  pntpbnd2  27947  f1otrg  29481  f1otrge  29482  brbtwn2  29516  ax5seglem3  29542  axpaschlem  29551  axcontlem7  29581  pthhashvtx  30348  hstel2  32854  stle1  32860  stj  32870  neldifpr2  33205  xrge0adddir  33655  slmdlema  33840  lmodslmd  33841  fldgensdrg  33960  rhmimaidl  34066  irngnzply1lem  34405  xrge0iifcnv  34648  xrge0iifiso  34650  xrge0iifhom  34652  rrextcusp  34720  rrextust  34723  unelros  34887  difelros  34888  inelsros  34894  diffiunisros  34895  sibfinima  35054  eulerpartlemf  35085  eulerpartlemgvv  35091  bnj563  35457  bnj1366  35542  bnj1379  35543  bnj554  35612  bnj557  35614  bnj570  35618  bnj594  35625  bnj1001  35672  bnj1006  35673  bnj1097  35694  bnj1177  35719  bnj1388  35746  bnj1398  35747  bnj1450  35763  bnj1501  35780  bnj1523  35784  snmlflim  36277  msrval  36483  mclsssvlem  36507  mclsind  36515  ptrecube  38743  cntotbnd  38933  heiborlem8  38955  dmnnzd  39212  eqvreltrrel  39819  atlex  40576  kelac1  44269  binomcxplemcvg  45541  binomcxplemnotnn0  45543  dmstructnn  46130  dmstructfi  46131  elixpconstg  46319  fvixp2  46428  stoweidlem39  47264  stoweidlem60  47285  fourierdlem40  47372  fourierdlem78  47409  idomnzd  49658  arweuthinc  50879