Theorem simp3bi 1146

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  limuni  6330  smores2  8194  ersym  8519  ertr  8522  fvixp  8699  undifixp  8731  fiint  9100  winalim2  10461  inar1  10540  supmullem1  11954  supmullem2  11955  supmul  11956  eluzle  12604  ico01fl0  13548  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  sin01gt0  15908  divalglem6  16116  gznegcl  16645  gzcjcl  16646  gzaddcl  16647  gzmulcl  16648  gzabssqcl  16651  4sqlem4a  16661  prdsbasprj  17192  xpsff1o  17287  mreintcl  17313  drsdir  18029  subggrp  18767  pmtrfconj  19083  symggen  19087  psgnunilem1  19110  subgpgp  19211  slwispgp  19225  sylow2alem1  19231  oppglsm  19256  efgsdmi  19347  efgsrel  19349  efgsp1  19352  efgsres  19353  efgcpbllemb  19370  efgcpbl  19371  srgi  19756  srgrz  19771  srglz  19772  ringi  19808  ringsrg  19837  irredmul  19960  sdrgint  20081  primefld  20082  lmodlema  20137  lsscl  20213  phllmhm  20846  ipcj  20848  ipeq0  20852  ocvi  20883  obsip  20937  obsocv  20942  2ndcctbss  22615  locfinnei  22683  fclssscls  23178  tmdcn  23243  tgpinv  23245  trgtmd  23325  tdrgunit  23327  ngpds  23769  nrmtngdist  23830  elii1  24107  elii2  24108  icopnfcnv  24114  icopnfhmeo  24115  iccpnfhmeo  24117  xrhmeo  24118  phtpcer  24167  pcoass  24196  clmsubrg  24238  cphnmfval  24365  bnsca  24512  uc1pldg  25322  mon1pldg  25323  sinq12ge0  25674  cosq14gt0  25676  cosq14ge0  25677  cos02pilt1  25691  cosq34lt1  25692  sinord  25699  recosf1o  25700  resinf1o  25701  logrnaddcl  25739  logimul  25778  dvlog2lem  25816  atanf  26039  atanneg  26066  atancj  26069  efiatan  26071  atanlogaddlem  26072  atanlogadd  26073  atanlogsub  26075  efiatan2  26076  2efiatan  26077  ressatans  26093  dvatan  26094  areaf  26120  harmonicubnd  26168  harmonicbnd4  26169  lgamgulmlem2  26188  2sqlem2  26575  2sqlem3  26577  dchrvmasumiflem1  26658  pntpbnd2  26744  f1otrg  27241  f1otrge  27242  brbtwn2  27282  ax5seglem3  27308  axpaschlem  27317  axcontlem7  27347  hstel2  30590  stle1  30596  stj  30606  neldifpr2  30891  xrge0adddir  31310  omndadd  31341  slmdlema  31465  lmodslmd  31466  orngmul  31511  rhmimaidl  31618  xrge0iifcnv  31892  xrge0iifiso  31894  xrge0iifhom  31896  rrextcusp  31964  rrextust  31967  unelros  32148  difelros  32149  inelsros  32155  diffiunisros  32156  sibfinima  32315  eulerpartlemf  32346  eulerpartlemgvv  32352  bnj563  32732  bnj1366  32818  bnj1379  32819  bnj554  32888  bnj557  32890  bnj570  32894  bnj594  32901  bnj1001  32948  bnj1006  32949  bnj1097  32970  bnj1177  32995  bnj1388  33022  bnj1398  33023  bnj1450  33039  bnj1501  33056  bnj1523  33060  pthhashvtx  33098  snmlflim  33303  msrval  33509  mclsssvlem  33533  mclsind  33541  ptrecube  35786  cntotbnd  35963  heiborlem8  35985  dmnnzd  36242  eqvreltrrel  36720  atlex  37337  kelac1  40895  binomcxplemcvg  41979  binomcxplemnotnn0  41981  elixpconstg  42646  fvixp2  42745  stoweidlem39  43587  stoweidlem60  43608  fourierdlem40  43695  fourierdlem78  43732  isringrng  45450