Theorem simp3bi 1078

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  limuni  5785  smores2  7451  ersym  7754  ertr  7757  fvixp  7913  undifixp  7944  fiint  8237  winalim2  9518  inar1  9597  supmullem1  10993  supmullem2  10994  supmul  10995  eluzle  11700  ico01fl0  12620  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  sin01gt0  14920  divalglem6  15121  gznegcl  15639  gzcjcl  15640  gzaddcl  15641  gzmulcl  15642  gzabssqcl  15645  4sqlem4a  15655  prdsbasprj  16132  xpsff1o  16228  mreintcl  16255  drsdir  16935  subggrp  17597  pmtrfconj  17886  symggen  17890  psgnunilem1  17913  subgpgp  18012  slwispgp  18026  sylow2alem1  18032  oppglsm  18057  efgsdmi  18145  efgsrel  18147  efgsp1  18150  efgsres  18151  efgcpbllemb  18168  efgcpbl  18169  srgi  18511  srgrz  18526  srglz  18527  ringi  18560  ringsrg  18589  irredmul  18709  lmodlema  18868  lsscl  18943  phllmhm  19977  ipcj  19979  ipeq0  19983  ocvi  20013  obsip  20065  obsocv  20070  2ndcctbss  21258  locfinnei  21326  fclssscls  21822  tmdcn  21887  tgpinv  21889  trgtmd  21968  tdrgunit  21970  ngpds  22408  nrmtngdist  22461  elii1  22734  elii2  22735  icopnfcnv  22741  icopnfhmeo  22742  iccpnfhmeo  22744  xrhmeo  22745  phtpcer  22794  phtpcerOLD  22795  pcoass  22824  clmsubrg  22866  cphnmfval  22992  bnsca  23136  uc1pldg  23908  mon1pldg  23909  sinq12ge0  24260  cosq14gt0  24262  cosq14ge0  24263  sinord  24280  recosf1o  24281  resinf1o  24282  logrnaddcl  24321  logimul  24360  dvlog2lem  24398  atanf  24607  atanneg  24634  atancj  24637  efiatan  24639  atanlogaddlem  24640  atanlogadd  24641  atanlogsub  24643  efiatan2  24644  2efiatan  24645  ressatans  24661  dvatan  24662  areaf  24688  harmonicubnd  24736  harmonicbnd4  24737  lgamgulmlem2  24756  2sqlem2  25143  2sqlem3  25145  dchrvmasumiflem1  25190  pntpbnd2  25276  f1otrg  25751  f1otrge  25752  brbtwn2  25785  ax5seglem3  25811  axpaschlem  25820  axcontlem7  25850  hstel2  29078  stle1  29084  stj  29094  xrge0adddir  29692  omndadd  29706  slmdlema  29756  lmodslmd  29757  orngmul  29803  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  rrextcusp  30049  rrextust  30052  unelros  30234  difelros  30235  inelsros  30241  diffiunisros  30242  sibfinima  30401  eulerpartlemf  30432  eulerpartlemgvv  30438  bnj563  30813  bnj1366  30900  bnj1379  30901  bnj554  30969  bnj557  30971  bnj570  30975  bnj594  30982  bnj1001  31028  bnj1006  31029  bnj1097  31049  bnj1177  31074  bnj1388  31101  bnj1398  31102  bnj1450  31118  bnj1501  31135  bnj1523  31139  snmlflim  31314  msrval  31435  mclsssvlem  31459  mclsind  31467  ptrecube  33409  cntotbnd  33595  heiborlem8  33617  dmnnzd  33874  atlex  34603  kelac1  37633  binomcxplemcvg  38553  binomcxplemnotnn0  38555  elixpconstg  39266  fvixp2  39389  stoweidlem39  40256  stoweidlem60  40277  fourierdlem40  40364  fourierdlem78  40401  isringrng  41881