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  8280  ersym  8640  ertr  8643  fvixp  8832  undifixp  8864  fiint  9218  winalim2  10594  inar1  10673  supmullem1  12099  supmullem2  12100  supmul  12101  eluzle  12751  ico01fl0  13725  ef01bndlem  16095  sin01bnd  16096  cos01bnd  16097  sin01gt0  16101  divalglem6  16311  gznegcl  16849  gzcjcl  16850  gzaddcl  16851  gzmulcl  16852  gzabssqcl  16855  4sqlem4a  16865  prdsbasprj  17378  xpsff1o  17473  mreintcl  17499  drsdir  18210  subggrp  19044  pmtrfconj  19380  symggen  19384  psgnunilem1  19407  subgpgp  19511  slwispgp  19525  sylow2alem1  19531  oppglsm  19556  efgsdmi  19646  efgsrel  19648  efgsp1  19651  efgsres  19652  efgcpbllemb  19669  efgcpbl  19670  omndadd  20042  srgdilem  20112  srgrz  20127  srglz  20128  ringdilem  20169  isringrng  20207  ringsrg  20217  irredmul  20349  subrngss  20465  sdrgdrng  20707  fldsdrgfld  20715  sdrgint  20721  primefld  20722  orngmul  20782  lmodlema  20800  lsscl  20877  phllmhm  21571  ipcj  21573  ipeq0  21577  ocvi  21608  obsip  21660  obsocv  21665  2ndcctbss  23371  locfinnei  23439  fclssscls  23934  tmdcn  23999  tgpinv  24001  trgtmd  24081  tdrgunit  24083  ngpds  24520  nrmtngdist  24573  elii1  24859  elii2  24860  icopnfcnv  24868  icopnfhmeo  24869  iccpnfhmeo  24871  xrhmeo  24872  phtpcer  24922  pcoass  24952  clmsubrg  24994  cphnmfval  25120  bnsca  25267  uc1pldg  26082  mon1pldg  26083  sinq12ge0  26445  cosq14gt0  26447  cosq14ge0  26448  cos02pilt1  26463  cosq34lt1  26464  sinord  26471  recosf1o  26472  resinf1o  26473  logrnaddcl  26511  logimul  26551  dvlog2lem  26589  atanf  26818  atanneg  26845  atancj  26848  efiatan  26850  atanlogaddlem  26851  atanlogadd  26852  atanlogsub  26854  efiatan2  26855  2efiatan  26856  ressatans  26872  dvatan  26873  areaf  26899  harmonicubnd  26948  harmonicbnd4  26949  lgamgulmlem2  26968  2sqlem2  27357  2sqlem3  27359  dchrvmasumiflem1  27440  pntpbnd2  27526  f1otrg  28850  f1otrge  28851  brbtwn2  28885  ax5seglem3  28911  axpaschlem  28920  axcontlem7  28950  hstel2  32201  stle1  32207  stj  32217  neldifpr2  32516  xrge0adddir  33006  slmdlema  33179  lmodslmd  33180  fldgensdrg  33287  rhmimaidl  33404  irngnzply1lem  33724  xrge0iifcnv  33967  xrge0iifiso  33969  xrge0iifhom  33971  rrextcusp  34039  rrextust  34042  unelros  34205  difelros  34206  inelsros  34212  diffiunisros  34213  sibfinima  34373  eulerpartlemf  34404  eulerpartlemgvv  34410  bnj563  34776  bnj1366  34862  bnj1379  34863  bnj554  34932  bnj557  34934  bnj570  34938  bnj594  34945  bnj1001  34992  bnj1006  34993  bnj1097  35014  bnj1177  35039  bnj1388  35066  bnj1398  35067  bnj1450  35083  bnj1501  35100  bnj1523  35104  pthhashvtx  35193  snmlflim  35397  msrval  35603  mclsssvlem  35627  mclsind  35635  ptrecube  37680  cntotbnd  37856  heiborlem8  37878  dmnnzd  38135  eqvreltrrel  38716  atlex  39435  kelac1  43180  binomcxplemcvg  44471  binomcxplemnotnn0  44473  elixpconstg  45210  fvixp2  45320  stoweidlem39  46161  stoweidlem60  46182  fourierdlem40  46269  fourierdlem78  46306  arweuthinc  49654