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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  limuni  6383  smores2  8305  ersym  8667  ertr  8670  fvixp  8847  undifixp  8879  fiint  9275  winalim2  10641  inar1  10720  supmullem1  12134  supmullem2  12135  supmul  12136  eluzle  12785  ico01fl0  13734  ef01bndlem  16077  sin01bnd  16078  cos01bnd  16079  sin01gt0  16083  divalglem6  16291  gznegcl  16818  gzcjcl  16819  gzaddcl  16820  gzmulcl  16821  gzabssqcl  16824  4sqlem4a  16834  prdsbasprj  17368  xpsff1o  17463  mreintcl  17489  drsdir  18205  subggrp  18945  pmtrfconj  19262  symggen  19266  psgnunilem1  19289  subgpgp  19393  slwispgp  19407  sylow2alem1  19413  oppglsm  19438  efgsdmi  19528  efgsrel  19530  efgsp1  19533  efgsres  19534  efgcpbllemb  19551  efgcpbl  19552  srgdilem  19937  srgrz  19952  srglz  19953  ringdilem  19994  ringsrg  20027  irredmul  20154  sdrgdrng  20313  fldsdrgfld  20321  sdrgint  20327  primefld  20328  lmodlema  20383  lsscl  20460  phllmhm  21073  ipcj  21075  ipeq0  21079  ocvi  21110  obsip  21164  obsocv  21169  2ndcctbss  22843  locfinnei  22911  fclssscls  23406  tmdcn  23471  tgpinv  23473  trgtmd  23553  tdrgunit  23555  ngpds  23997  nrmtngdist  24058  elii1  24335  elii2  24336  icopnfcnv  24342  icopnfhmeo  24343  iccpnfhmeo  24345  xrhmeo  24346  phtpcer  24395  pcoass  24424  clmsubrg  24466  cphnmfval  24593  bnsca  24740  uc1pldg  25550  mon1pldg  25551  sinq12ge0  25902  cosq14gt0  25904  cosq14ge0  25905  cos02pilt1  25919  cosq34lt1  25920  sinord  25927  recosf1o  25928  resinf1o  25929  logrnaddcl  25967  logimul  26006  dvlog2lem  26044  atanf  26267  atanneg  26294  atancj  26297  efiatan  26299  atanlogaddlem  26300  atanlogadd  26301  atanlogsub  26303  efiatan2  26304  2efiatan  26305  ressatans  26321  dvatan  26322  areaf  26348  harmonicubnd  26396  harmonicbnd4  26397  lgamgulmlem2  26416  2sqlem2  26803  2sqlem3  26805  dchrvmasumiflem1  26886  pntpbnd2  26972  f1otrg  27876  f1otrge  27877  brbtwn2  27917  ax5seglem3  27943  axpaschlem  27952  axcontlem7  27982  hstel2  31224  stle1  31230  stj  31240  neldifpr2  31525  xrge0adddir  31953  omndadd  31984  slmdlema  32108  lmodslmd  32109  fldgensdrg  32152  orngmul  32169  rhmimaidl  32282  irngnzply1lem  32451  xrge0iifcnv  32603  xrge0iifiso  32605  xrge0iifhom  32607  rrextcusp  32675  rrextust  32678  unelros  32859  difelros  32860  inelsros  32866  diffiunisros  32867  sibfinima  33028  eulerpartlemf  33059  eulerpartlemgvv  33065  bnj563  33444  bnj1366  33530  bnj1379  33531  bnj554  33600  bnj557  33602  bnj570  33606  bnj594  33613  bnj1001  33660  bnj1006  33661  bnj1097  33682  bnj1177  33707  bnj1388  33734  bnj1398  33735  bnj1450  33751  bnj1501  33768  bnj1523  33772  pthhashvtx  33808  snmlflim  34013  msrval  34219  mclsssvlem  34243  mclsind  34251  ptrecube  36151  cntotbnd  36328  heiborlem8  36350  dmnnzd  36607  eqvreltrrel  37135  atlex  37851  kelac1  41448  binomcxplemcvg  42756  binomcxplemnotnn0  42758  elixpconstg  43421  fvixp2  43541  stoweidlem39  44400  stoweidlem60  44421  fourierdlem40  44508  fourierdlem78  44545  isringrng  46299