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  6387  smores2  8296  ersym  8658  ertr  8661  fvixp  8852  undifixp  8884  fiint  9239  winalim2  10619  inar1  10698  supmullem1  12124  supmullem2  12125  supmul  12126  eluzle  12776  ico01fl0  13751  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  sin01gt0  16127  divalglem6  16337  gznegcl  16875  gzcjcl  16876  gzaddcl  16877  gzmulcl  16878  gzabssqcl  16881  4sqlem4a  16891  prdsbasprj  17404  xpsff1o  17500  mreintcl  17526  drsdir  18237  subggrp  19071  pmtrfconj  19407  symggen  19411  psgnunilem1  19434  subgpgp  19538  slwispgp  19552  sylow2alem1  19558  oppglsm  19583  efgsdmi  19673  efgsrel  19675  efgsp1  19678  efgsres  19679  efgcpbllemb  19696  efgcpbl  19697  omndadd  20069  srgdilem  20139  srgrz  20154  srglz  20155  ringdilem  20196  isringrng  20234  ringsrg  20244  irredmul  20377  subrngss  20493  sdrgdrng  20735  fldsdrgfld  20743  sdrgint  20749  primefld  20750  orngmul  20810  lmodlema  20828  lsscl  20905  phllmhm  21599  ipcj  21601  ipeq0  21605  ocvi  21636  obsip  21688  obsocv  21693  2ndcctbss  23411  locfinnei  23479  fclssscls  23974  tmdcn  24039  tgpinv  24041  trgtmd  24121  tdrgunit  24123  ngpds  24560  nrmtngdist  24613  elii1  24899  elii2  24900  icopnfcnv  24908  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  phtpcer  24962  pcoass  24992  clmsubrg  25034  cphnmfval  25160  bnsca  25307  uc1pldg  26122  mon1pldg  26123  sinq12ge0  26485  cosq14gt0  26487  cosq14ge0  26488  cos02pilt1  26503  cosq34lt1  26504  sinord  26511  recosf1o  26512  resinf1o  26513  logrnaddcl  26551  logimul  26591  dvlog2lem  26629  atanf  26858  atanneg  26885  atancj  26888  efiatan  26890  atanlogaddlem  26891  atanlogadd  26892  atanlogsub  26894  efiatan2  26895  2efiatan  26896  ressatans  26912  dvatan  26913  areaf  26939  harmonicubnd  26988  harmonicbnd4  26989  lgamgulmlem2  27008  2sqlem2  27397  2sqlem3  27399  dchrvmasumiflem1  27480  pntpbnd2  27566  f1otrg  28955  f1otrge  28956  brbtwn2  28990  ax5seglem3  29016  axpaschlem  29025  axcontlem7  29055  hstel2  32306  stle1  32312  stj  32322  neldifpr2  32620  xrge0adddir  33110  slmdlema  33296  lmodslmd  33297  fldgensdrg  33407  rhmimaidl  33524  irngnzply1lem  33867  xrge0iifcnv  34110  xrge0iifiso  34112  xrge0iifhom  34114  rrextcusp  34182  rrextust  34185  unelros  34348  difelros  34349  inelsros  34355  diffiunisros  34356  sibfinima  34516  eulerpartlemf  34547  eulerpartlemgvv  34553  bnj563  34919  bnj1366  35004  bnj1379  35005  bnj554  35074  bnj557  35076  bnj570  35080  bnj594  35087  bnj1001  35134  bnj1006  35135  bnj1097  35156  bnj1177  35181  bnj1388  35208  bnj1398  35209  bnj1450  35225  bnj1501  35242  bnj1523  35246  pthhashvtx  35341  snmlflim  35545  msrval  35751  mclsssvlem  35775  mclsind  35783  ptrecube  37865  cntotbnd  38041  heiborlem8  38063  dmnnzd  38320  eqvreltrrel  38929  atlex  39686  kelac1  43414  binomcxplemcvg  44704  binomcxplemnotnn0  44706  elixpconstg  45442  fvixp2  45551  stoweidlem39  46391  stoweidlem60  46412  fourierdlem40  46499  fourierdlem78  46536  arweuthinc  49882