Theorem simp3bi 1163

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 1160	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  limuni  6412  smores2  8329  ersym  8695  ertr  8698  fvixp  8888  undifixp  8920  fiint  9274  winalim2  10669  inar1  10748  supmullem1  12173  supmullem2  12174  supmul  12175  eluzle  12863  ico01fl0  13840  ef01bndlem  16228  sin01bnd  16229  cos01bnd  16230  sin01gt0  16234  divalglem6  16444  gznegcl  16983  gzcjcl  16984  gzaddcl  16985  gzmulcl  16986  gzabssqcl  16989  4sqlem4a  16999  prdsbasprj  17513  xpsff1o  17609  mreintcl  17635  drsdir  18346  subggrp  19183  pmtrfconj  19524  symggen  19528  psgnunilem1  19551  subgpgp  19655  slwispgp  19669  sylow2alem1  19675  oppglsm  19700  efgsdmi  19790  efgsrel  19792  efgsp1  19795  efgsres  19796  efgcpbllemb  19813  efgcpbl  19814  omndadd  20186  srgdilem  20262  srgrz  20277  srglz  20278  ringdilem  20319  isringrng  20358  ringsrg  20368  irredmul  20499  subrngss  20621  sdrgdrng  20859  fldsdrgfld  20867  sdrgint  20873  primefld  20874  orngmul  20934  lmodlema  20952  lsscl  21029  phllmhm  21739  ipcj  21741  ipeq0  21745  ocvi  21776  obsip  21828  obsocv  21833  2ndcctbss  23569  locfinnei  23637  fclssscls  24132  tmdcn  24197  tgpinv  24199  trgtmd  24279  tdrgunit  24281  ngpds  24718  nrmtngdist  24771  elii1  25051  elii2  25052  icopnfcnv  25058  icopnfhmeo  25059  iccpnfhmeo  25061  xrhmeo  25062  phtpcer  25111  pcoass  25140  clmsubrg  25182  cphnmfval  25308  bnsca  25455  uc1pldg  26263  mon1pldg  26264  sinq12ge0  26627  cosq14gt0  26629  cosq14ge0  26630  cos02pilt1  26645  cosq34lt1  26646  sinord  26653  recosf1o  26654  resinf1o  26655  logrnaddcl  26693  logimul  26733  dvlog2lem  26771  atanf  26999  atanneg  27026  atancj  27029  efiatan  27031  atanlogaddlem  27032  atanlogadd  27033  atanlogsub  27035  efiatan2  27036  2efiatan  27037  ressatans  27053  dvatan  27054  areaf  27080  harmonicubnd  27128  harmonicbnd4  27129  lgamgulmlem2  27148  2sqlem2  27536  2sqlem3  27538  dchrvmasumiflem1  27619  pntpbnd2  27705  f1otrg  29125  f1otrge  29126  brbtwn2  29160  ax5seglem3  29186  axpaschlem  29195  axcontlem7  29225  hstel2  32476  stle1  32482  stj  32492  neldifpr2  32786  xrge0adddir  33246  slmdlema  33431  lmodslmd  33432  fldgensdrg  33545  rhmimaidl  33651  irngnzply1lem  33992  xrge0iifcnv  34235  xrge0iifiso  34237  xrge0iifhom  34239  rrextcusp  34307  rrextust  34310  unelros  34473  difelros  34474  inelsros  34480  diffiunisros  34481  sibfinima  34641  eulerpartlemf  34672  eulerpartlemgvv  34678  bnj563  35044  bnj1366  35129  bnj1379  35130  bnj554  35199  bnj557  35201  bnj570  35205  bnj594  35212  bnj1001  35259  bnj1006  35260  bnj1097  35281  bnj1177  35306  bnj1388  35333  bnj1398  35334  bnj1450  35350  bnj1501  35367  bnj1523  35371  pthhashvtx  35486  snmlflim  35690  msrval  35896  mclsssvlem  35920  mclsind  35928  ptrecube  38126  cntotbnd  38302  heiborlem8  38324  dmnnzd  38581  eqvreltrrel  39190  atlex  39947  kelac1  43647  binomcxplemcvg  44923  binomcxplemnotnn0  44925  elixpconstg  45666  fvixp2  45775  stoweidlem39  46612  stoweidlem60  46633  fourierdlem40  46720  fourierdlem78  46757  arweuthinc  50159