Theorem simp3bi 1071

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  limuni  5702  smores2  7338  ersym  7641  ertr  7644  fvixp  7799  undifixp  7830  fiint  8122  winalim2  9397  inar1  9476  supmullem1  10870  supmullem2  10871  supmul  10872  eluzle  11576  ico01fl0  12482  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  sin01gt0  14759  divalglem6  14959  gznegcl  15477  gzcjcl  15478  gzaddcl  15479  gzmulcl  15480  gzabssqcl  15483  4sqlem4a  15493  prdsbasprj  15955  xpsff1o  16051  mreintcl  16078  drsdir  16758  subggrp  17420  pmtrfconj  17709  symggen  17713  psgnunilem1  17736  subgpgp  17835  slwispgp  17849  sylow2alem1  17855  oppglsm  17880  efgsdmi  17968  efgsrel  17970  efgsp1  17973  efgsres  17974  efgcpbllemb  17991  efgcpbl  17992  srgi  18334  srgrz  18349  srglz  18350  ringi  18383  ringsrg  18412  irredmul  18532  lmodlema  18691  lsscl  18764  phllmhm  19796  ipcj  19798  ipeq0  19802  ocvi  19832  obsip  19884  obsocv  19889  2ndcctbss  21068  locfinnei  21136  fclssscls  21632  tmdcn  21697  tgpinv  21699  trgtmd  21778  tdrgunit  21780  ngpds  22218  nrmtngdist  22271  elii1  22542  elii2  22543  icopnfcnv  22549  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  phtpcer  22602  phtpcerOLD  22603  pcoass  22632  clmsubrg  22674  cphnmfval  22800  bnsca  22944  uc1pldg  23712  mon1pldg  23713  sinq12ge0  24064  cosq14gt0  24066  cosq14ge0  24067  sinord  24084  recosf1o  24085  resinf1o  24086  logrnaddcl  24125  logimul  24164  dvlog2lem  24198  atanf  24407  atanneg  24434  atancj  24437  efiatan  24439  atanlogaddlem  24440  atanlogadd  24441  atanlogsub  24443  efiatan2  24444  2efiatan  24445  ressatans  24461  dvatan  24462  areaf  24488  harmonicubnd  24536  harmonicbnd4  24537  lgamgulmlem2  24556  2sqlem2  24943  2sqlem3  24945  dchrvmasumiflem1  24990  pntpbnd2  25076  f1otrg  25551  f1otrge  25552  brbtwn2  25585  ax5seglem3  25611  axpaschlem  25620  axcontlem7  25650  hstel2  28462  stle1  28468  stj  28478  xrge0adddir  29023  omndadd  29037  slmdlema  29087  lmodslmd  29088  orngmul  29134  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  rrextcusp  29377  rrextust  29380  unelros  29561  difelros  29562  inelsros  29568  diffiunisros  29569  sibfinima  29728  eulerpartlemf  29759  eulerpartlemgvv  29765  bnj563  30067  bnj1366  30154  bnj1379  30155  bnj554  30223  bnj557  30225  bnj570  30229  bnj594  30236  bnj1001  30282  bnj1006  30283  bnj1097  30303  bnj1177  30328  bnj1388  30355  bnj1398  30356  bnj1450  30372  bnj1501  30389  bnj1523  30393  snmlflim  30568  msrval  30689  mclsssvlem  30713  mclsind  30721  ptrecube  32579  cntotbnd  32765  heiborlem8  32787  dmnnzd  33044  atlex  33621  kelac1  36651  binomcxplemcvg  37575  binomcxplemnotnn0  37577  elixpconstg  38294  stoweidlem39  38932  stoweidlem60  38953  fourierdlem40  39040  fourierdlem78  39077  isringrng  41671