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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  limuni  6426  smores2  8354  ersym  8715  ertr  8718  fvixp  8896  undifixp  8928  fiint  9324  winalim2  10691  inar1  10770  supmullem1  12184  supmullem2  12185  supmul  12186  eluzle  12835  ico01fl0  13784  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  sin01gt0  16133  divalglem6  16341  gznegcl  16868  gzcjcl  16869  gzaddcl  16870  gzmulcl  16871  gzabssqcl  16874  4sqlem4a  16884  prdsbasprj  17418  xpsff1o  17513  mreintcl  17539  drsdir  18255  subggrp  19009  pmtrfconj  19334  symggen  19338  psgnunilem1  19361  subgpgp  19465  slwispgp  19479  sylow2alem1  19485  oppglsm  19510  efgsdmi  19600  efgsrel  19602  efgsp1  19605  efgsres  19606  efgcpbllemb  19623  efgcpbl  19624  srgdilem  20015  srgrz  20030  srglz  20031  ringdilem  20072  ringsrg  20109  irredmul  20243  sdrgdrng  20406  fldsdrgfld  20414  sdrgint  20420  primefld  20421  lmodlema  20476  lsscl  20553  phllmhm  21185  ipcj  21187  ipeq0  21191  ocvi  21222  obsip  21276  obsocv  21281  2ndcctbss  22959  locfinnei  23027  fclssscls  23522  tmdcn  23587  tgpinv  23589  trgtmd  23669  tdrgunit  23671  ngpds  24113  nrmtngdist  24174  elii1  24451  elii2  24452  icopnfcnv  24458  icopnfhmeo  24459  iccpnfhmeo  24461  xrhmeo  24462  phtpcer  24511  pcoass  24540  clmsubrg  24582  cphnmfval  24709  bnsca  24856  uc1pldg  25666  mon1pldg  25667  sinq12ge0  26018  cosq14gt0  26020  cosq14ge0  26021  cos02pilt1  26035  cosq34lt1  26036  sinord  26043  recosf1o  26044  resinf1o  26045  logrnaddcl  26083  logimul  26122  dvlog2lem  26160  atanf  26385  atanneg  26412  atancj  26415  efiatan  26417  atanlogaddlem  26418  atanlogadd  26419  atanlogsub  26421  efiatan2  26422  2efiatan  26423  ressatans  26439  dvatan  26440  areaf  26466  harmonicubnd  26514  harmonicbnd4  26515  lgamgulmlem2  26534  2sqlem2  26921  2sqlem3  26923  dchrvmasumiflem1  27004  pntpbnd2  27090  f1otrg  28122  f1otrge  28123  brbtwn2  28163  ax5seglem3  28189  axpaschlem  28198  axcontlem7  28228  hstel2  31472  stle1  31478  stj  31488  neldifpr2  31771  xrge0adddir  32193  omndadd  32224  slmdlema  32348  lmodslmd  32349  fldgensdrg  32404  orngmul  32421  rhmimaidl  32550  irngnzply1lem  32754  xrge0iifcnv  32913  xrge0iifiso  32915  xrge0iifhom  32917  rrextcusp  32985  rrextust  32988  unelros  33169  difelros  33170  inelsros  33176  diffiunisros  33177  sibfinima  33338  eulerpartlemf  33369  eulerpartlemgvv  33375  bnj563  33754  bnj1366  33840  bnj1379  33841  bnj554  33910  bnj557  33912  bnj570  33916  bnj594  33923  bnj1001  33970  bnj1006  33971  bnj1097  33992  bnj1177  34017  bnj1388  34044  bnj1398  34045  bnj1450  34061  bnj1501  34078  bnj1523  34082  pthhashvtx  34118  snmlflim  34323  msrval  34529  mclsssvlem  34553  mclsind  34561  ptrecube  36488  cntotbnd  36664  heiborlem8  36686  dmnnzd  36943  eqvreltrrel  37470  atlex  38186  kelac1  41805  binomcxplemcvg  43113  binomcxplemnotnn0  43115  elixpconstg  43778  fvixp2  43898  stoweidlem39  44755  stoweidlem60  44776  fourierdlem40  44863  fourierdlem78  44900  isringrng  46657  subrngss  46727