Theorem simp3bi 1147

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  limuni  6394  smores2  8323  ersym  8683  ertr  8686  fvixp  8875  undifixp  8907  fiint  9277  fiintOLD  9278  winalim2  10649  inar1  10728  supmullem1  12153  supmullem2  12154  supmul  12155  eluzle  12806  ico01fl0  13781  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  sin01gt0  16158  divalglem6  16368  gznegcl  16906  gzcjcl  16907  gzaddcl  16908  gzmulcl  16909  gzabssqcl  16912  4sqlem4a  16922  prdsbasprj  17435  xpsff1o  17530  mreintcl  17556  drsdir  18263  subggrp  19061  pmtrfconj  19396  symggen  19400  psgnunilem1  19423  subgpgp  19527  slwispgp  19541  sylow2alem1  19547  oppglsm  19572  efgsdmi  19662  efgsrel  19664  efgsp1  19667  efgsres  19668  efgcpbllemb  19685  efgcpbl  19686  srgdilem  20101  srgrz  20116  srglz  20117  ringdilem  20158  isringrng  20196  ringsrg  20206  irredmul  20338  subrngss  20457  sdrgdrng  20699  fldsdrgfld  20707  sdrgint  20713  primefld  20714  lmodlema  20771  lsscl  20848  phllmhm  21541  ipcj  21543  ipeq0  21547  ocvi  21578  obsip  21630  obsocv  21635  2ndcctbss  23342  locfinnei  23410  fclssscls  23905  tmdcn  23970  tgpinv  23972  trgtmd  24052  tdrgunit  24054  ngpds  24492  nrmtngdist  24545  elii1  24831  elii2  24832  icopnfcnv  24840  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  phtpcer  24894  pcoass  24924  clmsubrg  24966  cphnmfval  25092  bnsca  25239  uc1pldg  26054  mon1pldg  26055  sinq12ge0  26417  cosq14gt0  26419  cosq14ge0  26420  cos02pilt1  26435  cosq34lt1  26436  sinord  26443  recosf1o  26444  resinf1o  26445  logrnaddcl  26483  logimul  26523  dvlog2lem  26561  atanf  26790  atanneg  26817  atancj  26820  efiatan  26822  atanlogaddlem  26823  atanlogadd  26824  atanlogsub  26826  efiatan2  26827  2efiatan  26828  ressatans  26844  dvatan  26845  areaf  26871  harmonicubnd  26920  harmonicbnd4  26921  lgamgulmlem2  26940  2sqlem2  27329  2sqlem3  27331  dchrvmasumiflem1  27412  pntpbnd2  27498  f1otrg  28798  f1otrge  28799  brbtwn2  28832  ax5seglem3  28858  axpaschlem  28867  axcontlem7  28897  hstel2  32148  stle1  32154  stj  32164  neldifpr2  32463  xrge0adddir  32959  omndadd  33020  slmdlema  33156  lmodslmd  33157  fldgensdrg  33264  orngmul  33281  rhmimaidl  33403  irngnzply1lem  33685  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  rrextcusp  33995  rrextust  33998  unelros  34161  difelros  34162  inelsros  34168  diffiunisros  34169  sibfinima  34330  eulerpartlemf  34361  eulerpartlemgvv  34367  bnj563  34733  bnj1366  34819  bnj1379  34820  bnj554  34889  bnj557  34891  bnj570  34895  bnj594  34902  bnj1001  34949  bnj1006  34950  bnj1097  34971  bnj1177  34996  bnj1388  35023  bnj1398  35024  bnj1450  35040  bnj1501  35057  bnj1523  35061  pthhashvtx  35115  snmlflim  35319  msrval  35525  mclsssvlem  35549  mclsind  35557  ptrecube  37614  cntotbnd  37790  heiborlem8  37812  dmnnzd  38069  eqvreltrrel  38591  atlex  39309  kelac1  43052  binomcxplemcvg  44343  binomcxplemnotnn0  44345  elixpconstg  45083  fvixp2  45193  stoweidlem39  46037  stoweidlem60  46058  fourierdlem40  46145  fourierdlem78  46182  arweuthinc  49518