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  6418  smores2  8346  ersym  8714  ertr  8717  fvixp  8914  undifixp  8946  fiint  9302  winalim2  10762  inar1  10841  supmullem1  12268  supmullem2  12269  supmul  12270  eluzle  12959  ico01fl0  13939  ef01bndlem  16332  sin01bnd  16333  cos01bnd  16334  sin01gt0  16338  divalglem6  16548  gznegcl  17093  gzcjcl  17094  gzaddcl  17095  gzmulcl  17096  gzabssqcl  17099  4sqlem4a  17109  prdsbasprj  17623  xpsff1o  17719  mreintcl  17745  drsdir  18456  subggrp  19319  pmtrfconj  19660  symggen  19664  psgnunilem1  19687  subgpgp  19791  slwispgp  19805  sylow2alem1  19811  oppglsm  19836  efgsdmi  19926  efgsrel  19928  efgsp1  19931  efgsres  19932  efgcpbllemb  19949  efgcpbl  19950  omndadd  20322  srgdilem  20398  srgrz  20413  srglz  20414  ringdilem  20456  isringrng  20496  dfring2  20497  ringsrg  20508  irredmul  20639  subrngss  20780  sdrgdrng  21027  fldsdrgfld  21035  sdrgint  21041  primefld  21042  orngmul  21102  lmodlema  21120  lsscl  21197  phllmhm  21918  ipcj  21920  ipeq0  21924  ocvi  21955  obsip  22007  obsocv  22012  2ndcctbss  23754  locfinnei  23822  fclssscls  24317  tmdcn  24382  tgpinv  24384  trgtmd  24464  tdrgunit  24466  ngpds  24903  nrmtngdist  24956  elii1  25236  elii2  25237  icopnfcnv  25243  icopnfhmeo  25244  iccpnfhmeo  25246  xrhmeo  25247  phtpcer  25296  pcoass  25325  clmsubrg  25367  cphnmfval  25493  bnsca  25640  uc1pldg  26447  mon1pldg  26448  sinq12ge0  26819  cosq14gt0  26821  cosq14ge0  26822  cos02pilt1  26836  cosq34lt1  26837  sinord  26844  recosf1o  26845  resinf1o  26846  logrnaddcl  26884  logimul  26924  dvlog2lem  26962  atanf  27190  atanneg  27217  atancj  27220  efiatan  27222  atanlogaddlem  27223  atanlogadd  27224  atanlogsub  27226  efiatan2  27227  2efiatan  27228  ressatans  27244  dvatan  27245  areaf  27271  harmonicubnd  27319  harmonicbnd4  27320  lgamgulmlem2  27339  2sqlem2  27727  2sqlem3  27729  dchrvmasumiflem1  27810  pntpbnd2  27896  f1otrg  29430  f1otrge  29431  brbtwn2  29465  ax5seglem3  29491  axpaschlem  29500  axcontlem7  29530  pthhashvtx  30297  hstel2  32803  stle1  32809  stj  32819  neldifpr2  33112  xrge0adddir  33561  slmdlema  33746  lmodslmd  33747  fldgensdrg  33858  rhmimaidl  33964  irngnzply1lem  34304  xrge0iifcnv  34547  xrge0iifiso  34549  xrge0iifhom  34551  rrextcusp  34619  rrextust  34622  unelros  34786  difelros  34787  inelsros  34793  diffiunisros  34794  sibfinima  34954  eulerpartlemf  34985  eulerpartlemgvv  34991  bnj563  35357  bnj1366  35442  bnj1379  35443  bnj554  35512  bnj557  35514  bnj570  35518  bnj594  35525  bnj1001  35572  bnj1006  35573  bnj1097  35594  bnj1177  35619  bnj1388  35646  bnj1398  35647  bnj1450  35663  bnj1501  35680  bnj1523  35684  snmlflim  36066  msrval  36272  mclsssvlem  36296  mclsind  36304  ptrecube  38506  cntotbnd  38698  heiborlem8  38720  dmnnzd  38977  eqvreltrrel  39584  atlex  40341  kelac1  44023  binomcxplemcvg  45297  binomcxplemnotnn0  45299  elixpconstg  46047  fvixp2  46156  stoweidlem39  46993  stoweidlem60  47014  fourierdlem40  47101  fourierdlem78  47138  idomnzd  49387  arweuthinc  50581