Theorem simp3bi 1143

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  limuni  6237  smores2  7977  ersym  8287  ertr  8290  fvixp  8452  undifixp  8484  fiint  8781  winalim2  10104  inar1  10183  supmullem1  11597  supmullem2  11598  supmul  11599  eluzle  12243  ico01fl0  13179  ef01bndlem  15522  sin01bnd  15523  cos01bnd  15524  sin01gt0  15528  divalglem6  15732  gznegcl  16254  gzcjcl  16255  gzaddcl  16256  gzmulcl  16257  gzabssqcl  16260  4sqlem4a  16270  prdsbasprj  16728  xpsff1o  16823  mreintcl  16849  drsdir  17528  subggrp  18265  pmtrfconj  18577  symggen  18581  psgnunilem1  18604  subgpgp  18705  slwispgp  18719  sylow2alem1  18725  oppglsm  18750  efgsdmi  18841  efgsrel  18843  efgsp1  18846  efgsres  18847  efgcpbllemb  18864  efgcpbl  18865  srgi  19244  srgrz  19259  srglz  19260  ringi  19293  ringsrg  19322  irredmul  19442  sdrgint  19566  primefld  19567  lmodlema  19622  lsscl  19697  phllmhm  20759  ipcj  20761  ipeq0  20765  ocvi  20796  obsip  20848  obsocv  20853  2ndcctbss  22046  locfinnei  22114  fclssscls  22609  tmdcn  22674  tgpinv  22676  trgtmd  22756  tdrgunit  22758  ngpds  23196  nrmtngdist  23249  elii1  23522  elii2  23523  icopnfcnv  23529  icopnfhmeo  23530  iccpnfhmeo  23532  xrhmeo  23533  phtpcer  23582  pcoass  23611  clmsubrg  23653  cphnmfval  23779  bnsca  23925  uc1pldg  24728  mon1pldg  24729  sinq12ge0  25080  cosq14gt0  25082  cosq14ge0  25083  cos02pilt1  25097  cosq34lt1  25098  sinord  25104  recosf1o  25105  resinf1o  25106  logrnaddcl  25144  logimul  25183  dvlog2lem  25221  atanf  25444  atanneg  25471  atancj  25474  efiatan  25476  atanlogaddlem  25477  atanlogadd  25478  atanlogsub  25480  efiatan2  25481  2efiatan  25482  ressatans  25498  dvatan  25499  areaf  25525  harmonicubnd  25573  harmonicbnd4  25574  lgamgulmlem2  25593  2sqlem2  25980  2sqlem3  25982  dchrvmasumiflem1  26063  pntpbnd2  26149  f1otrg  26643  f1otrge  26644  brbtwn2  26677  ax5seglem3  26703  axpaschlem  26712  axcontlem7  26742  hstel2  29980  stle1  29986  stj  29996  neldifpr2  30280  xrge0adddir  30686  omndadd  30714  slmdlema  30838  lmodslmd  30839  orngmul  30883  xrge0iifcnv  31183  xrge0iifiso  31185  xrge0iifhom  31187  rrextcusp  31253  rrextust  31256  unelros  31437  difelros  31438  inelsros  31444  diffiunisros  31445  sibfinima  31604  eulerpartlemf  31635  eulerpartlemgvv  31641  bnj563  32021  bnj1366  32108  bnj1379  32109  bnj554  32178  bnj557  32180  bnj570  32184  bnj594  32191  bnj1001  32238  bnj1006  32239  bnj1097  32260  bnj1177  32285  bnj1388  32312  bnj1398  32313  bnj1450  32329  bnj1501  32346  bnj1523  32350  pthhashvtx  32381  snmlflim  32586  msrval  32792  mclsssvlem  32816  mclsind  32824  ptrecube  34926  cntotbnd  35106  heiborlem8  35128  dmnnzd  35385  eqvreltrrel  35867  atlex  36484  kelac1  39755  binomcxplemcvg  40776  binomcxplemnotnn0  40778  elixpconstg  41445  fvixp2  41551  stoweidlem39  42414  stoweidlem60  42435  fourierdlem40  42522  fourierdlem78  42559  isringrng  44237