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  6379  smores2  8287  ersym  8649  ertr  8652  fvixp  8843  undifixp  8875  fiint  9230  winalim2  10610  inar1  10689  supmullem1  12117  supmullem2  12118  supmul  12119  eluzle  12792  ico01fl0  13769  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  sin01gt0  16148  divalglem6  16358  gznegcl  16897  gzcjcl  16898  gzaddcl  16899  gzmulcl  16900  gzabssqcl  16903  4sqlem4a  16913  prdsbasprj  17426  xpsff1o  17522  mreintcl  17548  drsdir  18259  subggrp  19096  pmtrfconj  19432  symggen  19436  psgnunilem1  19459  subgpgp  19563  slwispgp  19577  sylow2alem1  19583  oppglsm  19608  efgsdmi  19698  efgsrel  19700  efgsp1  19703  efgsres  19704  efgcpbllemb  19721  efgcpbl  19722  omndadd  20094  srgdilem  20164  srgrz  20179  srglz  20180  ringdilem  20221  isringrng  20259  ringsrg  20269  irredmul  20400  subrngss  20516  sdrgdrng  20758  fldsdrgfld  20766  sdrgint  20772  primefld  20773  orngmul  20833  lmodlema  20851  lsscl  20928  phllmhm  21622  ipcj  21624  ipeq0  21628  ocvi  21659  obsip  21711  obsocv  21716  2ndcctbss  23430  locfinnei  23498  fclssscls  23993  tmdcn  24058  tgpinv  24060  trgtmd  24140  tdrgunit  24142  ngpds  24579  nrmtngdist  24632  elii1  24912  elii2  24913  icopnfcnv  24919  icopnfhmeo  24920  iccpnfhmeo  24922  xrhmeo  24923  phtpcer  24972  pcoass  25001  clmsubrg  25043  cphnmfval  25169  bnsca  25316  uc1pldg  26124  mon1pldg  26125  sinq12ge0  26485  cosq14gt0  26487  cosq14ge0  26488  cos02pilt1  26503  cosq34lt1  26504  sinord  26511  recosf1o  26512  resinf1o  26513  logrnaddcl  26551  logimul  26591  dvlog2lem  26629  atanf  26857  atanneg  26884  atancj  26887  efiatan  26889  atanlogaddlem  26890  atanlogadd  26891  atanlogsub  26893  efiatan2  26894  2efiatan  26895  ressatans  26911  dvatan  26912  areaf  26938  harmonicubnd  26987  harmonicbnd4  26988  lgamgulmlem2  27007  2sqlem2  27395  2sqlem3  27397  dchrvmasumiflem1  27478  pntpbnd2  27564  f1otrg  28953  f1otrge  28954  brbtwn2  28988  ax5seglem3  29014  axpaschlem  29023  axcontlem7  29053  hstel2  32305  stle1  32311  stj  32321  neldifpr2  32619  xrge0adddir  33093  slmdlema  33279  lmodslmd  33280  fldgensdrg  33390  rhmimaidl  33507  irngnzply1lem  33850  xrge0iifcnv  34093  xrge0iifiso  34095  xrge0iifhom  34097  rrextcusp  34165  rrextust  34168  unelros  34331  difelros  34332  inelsros  34338  diffiunisros  34339  sibfinima  34499  eulerpartlemf  34530  eulerpartlemgvv  34536  bnj563  34902  bnj1366  34987  bnj1379  34988  bnj554  35057  bnj557  35059  bnj570  35063  bnj594  35070  bnj1001  35117  bnj1006  35118  bnj1097  35139  bnj1177  35164  bnj1388  35191  bnj1398  35192  bnj1450  35208  bnj1501  35225  bnj1523  35229  pthhashvtx  35326  snmlflim  35530  msrval  35736  mclsssvlem  35760  mclsind  35768  ptrecube  37955  cntotbnd  38131  heiborlem8  38153  dmnnzd  38410  eqvreltrrel  39019  atlex  39776  kelac1  43509  binomcxplemcvg  44799  binomcxplemnotnn0  44801  elixpconstg  45537  fvixp2  45646  stoweidlem39  46485  stoweidlem60  46506  fourierdlem40  46593  fourierdlem78  46630  arweuthinc  50016