Theorem simp3bi 1165

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  limuni  6430  smores2  8350  ersym  8716  ertr  8719  fvixp  8909  undifixp  8941  fiint  9296  winalim2  10699  inar1  10778  supmullem1  12203  supmullem2  12204  supmul  12205  eluzle  12893  ico01fl0  13872  ef01bndlem  16265  sin01bnd  16266  cos01bnd  16267  sin01gt0  16271  divalglem6  16481  gznegcl  17020  gzcjcl  17021  gzaddcl  17022  gzmulcl  17023  gzabssqcl  17026  4sqlem4a  17036  prdsbasprj  17550  xpsff1o  17646  mreintcl  17672  drsdir  18383  subggrp  19226  pmtrfconj  19567  symggen  19571  psgnunilem1  19594  subgpgp  19698  slwispgp  19712  sylow2alem1  19718  oppglsm  19743  efgsdmi  19833  efgsrel  19835  efgsp1  19838  efgsres  19839  efgcpbllemb  19856  efgcpbl  19857  omndadd  20229  srgdilem  20305  srgrz  20320  srglz  20321  ringdilem  20362  isringrng  20402  dfring2  20403  ringsrg  20413  irredmul  20544  subrngss  20684  sdrgdrng  20930  fldsdrgfld  20938  sdrgint  20944  primefld  20945  orngmul  21005  lmodlema  21023  lsscl  21100  phllmhm  21819  ipcj  21821  ipeq0  21825  ocvi  21856  obsip  21908  obsocv  21913  2ndcctbss  23649  locfinnei  23717  fclssscls  24212  tmdcn  24277  tgpinv  24279  trgtmd  24359  tdrgunit  24361  ngpds  24798  nrmtngdist  24851  elii1  25131  elii2  25132  icopnfcnv  25138  icopnfhmeo  25139  iccpnfhmeo  25141  xrhmeo  25142  phtpcer  25191  pcoass  25220  clmsubrg  25262  cphnmfval  25388  bnsca  25535  uc1pldg  26343  mon1pldg  26344  sinq12ge0  26710  cosq14gt0  26712  cosq14ge0  26713  cos02pilt1  26728  cosq34lt1  26729  sinord  26736  recosf1o  26737  resinf1o  26738  logrnaddcl  26776  logimul  26816  dvlog2lem  26854  atanf  27082  atanneg  27109  atancj  27112  efiatan  27114  atanlogaddlem  27115  atanlogadd  27116  atanlogsub  27118  efiatan2  27119  2efiatan  27120  ressatans  27136  dvatan  27137  areaf  27163  harmonicubnd  27211  harmonicbnd4  27212  lgamgulmlem2  27231  2sqlem2  27619  2sqlem3  27621  dchrvmasumiflem1  27702  pntpbnd2  27788  f1otrg  29257  f1otrge  29258  brbtwn2  29292  ax5seglem3  29318  axpaschlem  29327  axcontlem7  29357  hstel2  32608  stle1  32614  stj  32624  neldifpr2  32917  xrge0adddir  33369  slmdlema  33554  lmodslmd  33555  fldgensdrg  33666  rhmimaidl  33771  irngnzply1lem  34111  xrge0iifcnv  34354  xrge0iifiso  34356  xrge0iifhom  34358  rrextcusp  34426  rrextust  34429  unelros  34593  difelros  34594  inelsros  34600  diffiunisros  34601  sibfinima  34761  eulerpartlemf  34792  eulerpartlemgvv  34798  bnj563  35164  bnj1366  35249  bnj1379  35250  bnj554  35319  bnj557  35321  bnj570  35325  bnj594  35332  bnj1001  35379  bnj1006  35380  bnj1097  35401  bnj1177  35426  bnj1388  35453  bnj1398  35454  bnj1450  35470  bnj1501  35487  bnj1523  35491  pthhashvtx  35641  snmlflim  35845  msrval  36051  mclsssvlem  36075  mclsind  36083  ptrecube  38312  cntotbnd  38488  heiborlem8  38510  dmnnzd  38767  eqvreltrrel  39374  atlex  40131  kelac1  43831  binomcxplemcvg  45105  binomcxplemnotnn0  45107  elixpconstg  45848  fvixp2  45957  stoweidlem39  46794  stoweidlem60  46815  fourierdlem40  46902  fourierdlem78  46939  idomnzd  49152  arweuthinc  50348