Theorem simp3bi 1147

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

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

This theorem is referenced by:  limuni  6373  smores2  8284  ersym  8644  ertr  8647  fvixp  8836  undifixp  8868  fiint  9235  fiintOLD  9236  winalim2  10609  inar1  10688  supmullem1  12113  supmullem2  12114  supmul  12115  eluzle  12766  ico01fl0  13741  ef01bndlem  16111  sin01bnd  16112  cos01bnd  16113  sin01gt0  16117  divalglem6  16327  gznegcl  16865  gzcjcl  16866  gzaddcl  16867  gzmulcl  16868  gzabssqcl  16871  4sqlem4a  16881  prdsbasprj  17394  xpsff1o  17489  mreintcl  17515  drsdir  18226  subggrp  19026  pmtrfconj  19363  symggen  19367  psgnunilem1  19390  subgpgp  19494  slwispgp  19508  sylow2alem1  19514  oppglsm  19539  efgsdmi  19629  efgsrel  19631  efgsp1  19634  efgsres  19635  efgcpbllemb  19652  efgcpbl  19653  omndadd  20025  srgdilem  20095  srgrz  20110  srglz  20111  ringdilem  20152  isringrng  20190  ringsrg  20200  irredmul  20332  subrngss  20451  sdrgdrng  20693  fldsdrgfld  20701  sdrgint  20707  primefld  20708  orngmul  20768  lmodlema  20786  lsscl  20863  phllmhm  21557  ipcj  21559  ipeq0  21563  ocvi  21594  obsip  21646  obsocv  21651  2ndcctbss  23358  locfinnei  23426  fclssscls  23921  tmdcn  23986  tgpinv  23988  trgtmd  24068  tdrgunit  24070  ngpds  24508  nrmtngdist  24561  elii1  24847  elii2  24848  icopnfcnv  24856  icopnfhmeo  24857  iccpnfhmeo  24859  xrhmeo  24860  phtpcer  24910  pcoass  24940  clmsubrg  24982  cphnmfval  25108  bnsca  25255  uc1pldg  26070  mon1pldg  26071  sinq12ge0  26433  cosq14gt0  26435  cosq14ge0  26436  cos02pilt1  26451  cosq34lt1  26452  sinord  26459  recosf1o  26460  resinf1o  26461  logrnaddcl  26499  logimul  26539  dvlog2lem  26577  atanf  26806  atanneg  26833  atancj  26836  efiatan  26838  atanlogaddlem  26839  atanlogadd  26840  atanlogsub  26842  efiatan2  26843  2efiatan  26844  ressatans  26860  dvatan  26861  areaf  26887  harmonicubnd  26936  harmonicbnd4  26937  lgamgulmlem2  26956  2sqlem2  27345  2sqlem3  27347  dchrvmasumiflem1  27428  pntpbnd2  27514  f1otrg  28834  f1otrge  28835  brbtwn2  28868  ax5seglem3  28894  axpaschlem  28903  axcontlem7  28933  hstel2  32181  stle1  32187  stj  32197  neldifpr2  32496  xrge0adddir  32985  slmdlema  33155  lmodslmd  33156  fldgensdrg  33263  rhmimaidl  33379  irngnzply1lem  33661  xrge0iifcnv  33899  xrge0iifiso  33901  xrge0iifhom  33903  rrextcusp  33971  rrextust  33974  unelros  34137  difelros  34138  inelsros  34144  diffiunisros  34145  sibfinima  34306  eulerpartlemf  34337  eulerpartlemgvv  34343  bnj563  34709  bnj1366  34795  bnj1379  34796  bnj554  34865  bnj557  34867  bnj570  34871  bnj594  34878  bnj1001  34925  bnj1006  34926  bnj1097  34947  bnj1177  34972  bnj1388  34999  bnj1398  35000  bnj1450  35016  bnj1501  35033  bnj1523  35037  pthhashvtx  35100  snmlflim  35304  msrval  35510  mclsssvlem  35534  mclsind  35542  ptrecube  37599  cntotbnd  37775  heiborlem8  37797  dmnnzd  38054  eqvreltrrel  38576  atlex  39294  kelac1  43036  binomcxplemcvg  44327  binomcxplemnotnn0  44329  elixpconstg  45067  fvixp2  45177  stoweidlem39  46021  stoweidlem60  46042  fourierdlem40  46129  fourierdlem78  46166  arweuthinc  49515