Theorem simp3bi 1144

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

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

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 400  df-3an 1086

This theorem is referenced by:  limuni  6234  smores2  8007  ersym  8317  ertr  8320  fvixp  8497  undifixp  8529  fiint  8841  winalim2  10169  inar1  10248  supmullem1  11660  supmullem2  11661  supmul  11662  eluzle  12308  ico01fl0  13251  ef01bndlem  15598  sin01bnd  15599  cos01bnd  15600  sin01gt0  15604  divalglem6  15812  gznegcl  16340  gzcjcl  16341  gzaddcl  16342  gzmulcl  16343  gzabssqcl  16346  4sqlem4a  16356  prdsbasprj  16817  xpsff1o  16912  mreintcl  16938  drsdir  17625  subggrp  18363  pmtrfconj  18675  symggen  18679  psgnunilem1  18702  subgpgp  18803  slwispgp  18817  sylow2alem1  18823  oppglsm  18848  efgsdmi  18939  efgsrel  18941  efgsp1  18944  efgsres  18945  efgcpbllemb  18962  efgcpbl  18963  srgi  19343  srgrz  19358  srglz  19359  ringi  19395  ringsrg  19424  irredmul  19544  sdrgint  19665  primefld  19666  lmodlema  19721  lsscl  19796  phllmhm  20411  ipcj  20413  ipeq0  20417  ocvi  20448  obsip  20500  obsocv  20505  2ndcctbss  22169  locfinnei  22237  fclssscls  22732  tmdcn  22797  tgpinv  22799  trgtmd  22879  tdrgunit  22881  ngpds  23320  nrmtngdist  23373  elii1  23650  elii2  23651  icopnfcnv  23657  icopnfhmeo  23658  iccpnfhmeo  23660  xrhmeo  23661  phtpcer  23710  pcoass  23739  clmsubrg  23781  cphnmfval  23907  bnsca  24053  uc1pldg  24862  mon1pldg  24863  sinq12ge0  25214  cosq14gt0  25216  cosq14ge0  25217  cos02pilt1  25231  cosq34lt1  25232  sinord  25239  recosf1o  25240  resinf1o  25241  logrnaddcl  25279  logimul  25318  dvlog2lem  25356  atanf  25579  atanneg  25606  atancj  25609  efiatan  25611  atanlogaddlem  25612  atanlogadd  25613  atanlogsub  25615  efiatan2  25616  2efiatan  25617  ressatans  25633  dvatan  25634  areaf  25660  harmonicubnd  25708  harmonicbnd4  25709  lgamgulmlem2  25728  2sqlem2  26115  2sqlem3  26117  dchrvmasumiflem1  26198  pntpbnd2  26284  f1otrg  26778  f1otrge  26779  brbtwn2  26812  ax5seglem3  26838  axpaschlem  26847  axcontlem7  26877  hstel2  30115  stle1  30121  stj  30131  neldifpr2  30418  xrge0adddir  30840  omndadd  30871  slmdlema  30995  lmodslmd  30996  orngmul  31041  rhmimaidl  31143  xrge0iifcnv  31417  xrge0iifiso  31419  xrge0iifhom  31421  rrextcusp  31487  rrextust  31490  unelros  31671  difelros  31672  inelsros  31678  diffiunisros  31679  sibfinima  31838  eulerpartlemf  31869  eulerpartlemgvv  31875  bnj563  32255  bnj1366  32342  bnj1379  32343  bnj554  32412  bnj557  32414  bnj570  32418  bnj594  32425  bnj1001  32472  bnj1006  32473  bnj1097  32494  bnj1177  32519  bnj1388  32546  bnj1398  32547  bnj1450  32563  bnj1501  32580  bnj1523  32584  pthhashvtx  32618  snmlflim  32823  msrval  33029  mclsssvlem  33053  mclsind  33061  ptrecube  35372  cntotbnd  35549  heiborlem8  35571  dmnnzd  35828  eqvreltrrel  36310  atlex  36927  kelac1  40425  binomcxplemcvg  41476  binomcxplemnotnn0  41478  elixpconstg  42143  fvixp2  42242  stoweidlem39  43092  stoweidlem60  43113  fourierdlem40  43200  fourierdlem78  43237  isringrng  44931