Theorem simp3bi 1148

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

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

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 1089

This theorem is referenced by:  limuni  6445  smores2  8394  ersym  8757  ertr  8760  fvixp  8942  undifixp  8974  fiint  9366  fiintOLD  9367  winalim2  10736  inar1  10815  supmullem1  12238  supmullem2  12239  supmul  12240  eluzle  12891  ico01fl0  13859  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  sin01gt0  16226  divalglem6  16435  gznegcl  16973  gzcjcl  16974  gzaddcl  16975  gzmulcl  16976  gzabssqcl  16979  4sqlem4a  16989  prdsbasprj  17517  xpsff1o  17612  mreintcl  17638  drsdir  18348  subggrp  19147  pmtrfconj  19484  symggen  19488  psgnunilem1  19511  subgpgp  19615  slwispgp  19629  sylow2alem1  19635  oppglsm  19660  efgsdmi  19750  efgsrel  19752  efgsp1  19755  efgsres  19756  efgcpbllemb  19773  efgcpbl  19774  srgdilem  20189  srgrz  20204  srglz  20205  ringdilem  20246  isringrng  20284  ringsrg  20294  irredmul  20429  subrngss  20548  sdrgdrng  20791  fldsdrgfld  20799  sdrgint  20805  primefld  20806  lmodlema  20863  lsscl  20940  phllmhm  21650  ipcj  21652  ipeq0  21656  ocvi  21687  obsip  21741  obsocv  21746  2ndcctbss  23463  locfinnei  23531  fclssscls  24026  tmdcn  24091  tgpinv  24093  trgtmd  24173  tdrgunit  24175  ngpds  24617  nrmtngdist  24678  elii1  24964  elii2  24965  icopnfcnv  24973  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  phtpcer  25027  pcoass  25057  clmsubrg  25099  cphnmfval  25226  bnsca  25373  uc1pldg  26188  mon1pldg  26189  sinq12ge0  26550  cosq14gt0  26552  cosq14ge0  26553  cos02pilt1  26568  cosq34lt1  26569  sinord  26576  recosf1o  26577  resinf1o  26578  logrnaddcl  26616  logimul  26656  dvlog2lem  26694  atanf  26923  atanneg  26950  atancj  26953  efiatan  26955  atanlogaddlem  26956  atanlogadd  26957  atanlogsub  26959  efiatan2  26960  2efiatan  26961  ressatans  26977  dvatan  26978  areaf  27004  harmonicubnd  27053  harmonicbnd4  27054  lgamgulmlem2  27073  2sqlem2  27462  2sqlem3  27464  dchrvmasumiflem1  27545  pntpbnd2  27631  f1otrg  28879  f1otrge  28880  brbtwn2  28920  ax5seglem3  28946  axpaschlem  28955  axcontlem7  28985  hstel2  32238  stle1  32244  stj  32254  neldifpr2  32552  xrge0adddir  33023  omndadd  33083  slmdlema  33209  lmodslmd  33210  fldgensdrg  33316  orngmul  33333  rhmimaidl  33460  irngnzply1lem  33740  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  rrextcusp  34006  rrextust  34009  unelros  34172  difelros  34173  inelsros  34179  diffiunisros  34180  sibfinima  34341  eulerpartlemf  34372  eulerpartlemgvv  34378  bnj563  34757  bnj1366  34843  bnj1379  34844  bnj554  34913  bnj557  34915  bnj570  34919  bnj594  34926  bnj1001  34973  bnj1006  34974  bnj1097  34995  bnj1177  35020  bnj1388  35047  bnj1398  35048  bnj1450  35064  bnj1501  35081  bnj1523  35085  pthhashvtx  35133  snmlflim  35337  msrval  35543  mclsssvlem  35567  mclsind  35575  ptrecube  37627  cntotbnd  37803  heiborlem8  37825  dmnnzd  38082  eqvreltrrel  38601  atlex  39317  kelac1  43075  binomcxplemcvg  44373  binomcxplemnotnn0  44375  elixpconstg  45094  fvixp2  45204  stoweidlem39  46054  stoweidlem60  46075  fourierdlem40  46162  fourierdlem78  46199