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  6425  smores2  8366  ersym  8734  ertr  8737  fvixp  8934  undifixp  8966  fiint  9322  winalim2  10785  inar1  10864  supmullem1  12291  supmullem2  12292  supmul  12293  eluzle  12982  ico01fl0  13963  ef01bndlem  16358  sin01bnd  16359  cos01bnd  16360  sin01gt0  16364  divalglem6  16574  gznegcl  17119  gzcjcl  17120  gzaddcl  17121  gzmulcl  17122  gzabssqcl  17125  4sqlem4a  17135  prdsbasprj  17649  xpsff1o  17745  mreintcl  17771  drsdir  18482  subggrp  19345  pmtrfconj  19686  symggen  19690  psgnunilem1  19713  subgpgp  19817  slwispgp  19831  sylow2alem1  19837  oppglsm  19862  efgsdmi  19952  efgsrel  19954  efgsp1  19957  efgsres  19958  efgcpbllemb  19975  efgcpbl  19976  omndadd  20348  srgdilem  20424  srgrz  20439  srglz  20440  ringdilem  20482  isringrng  20522  dfring2  20523  ringsrg  20534  irredmul  20665  subrngss  20806  sdrgdrng  21053  fldsdrgfld  21061  sdrgint  21067  primefld  21068  orngmul  21128  lmodlema  21146  lsscl  21223  phllmhm  21944  ipcj  21946  ipeq0  21950  ocvi  21981  obsip  22033  obsocv  22038  2ndcctbss  23780  locfinnei  23848  fclssscls  24343  tmdcn  24408  tgpinv  24410  trgtmd  24490  tdrgunit  24492  ngpds  24929  nrmtngdist  24982  elii1  25262  elii2  25263  icopnfcnv  25269  icopnfhmeo  25270  iccpnfhmeo  25272  xrhmeo  25273  phtpcer  25322  pcoass  25351  clmsubrg  25393  cphnmfval  25519  bnsca  25666  uc1pldg  26473  mon1pldg  26474  sinq12ge0  26843  cosq14gt0  26845  cosq14ge0  26846  cos02pilt1  26860  cosq34lt1  26861  sinord  26868  recosf1o  26869  resinf1o  26870  logrnaddcl  26908  logimul  26948  dvlog2lem  26986  atanf  27214  atanneg  27241  atancj  27244  efiatan  27246  atanlogaddlem  27247  atanlogadd  27248  atanlogsub  27250  efiatan2  27251  2efiatan  27252  ressatans  27268  dvatan  27269  areaf  27295  harmonicubnd  27343  harmonicbnd4  27344  lgamgulmlem2  27363  2sqlem2  27751  2sqlem3  27753  dchrvmasumiflem1  27834  pntpbnd2  27920  f1otrg  29454  f1otrge  29455  brbtwn2  29489  ax5seglem3  29515  axpaschlem  29524  axcontlem7  29554  pthhashvtx  30321  hstel2  32827  stle1  32833  stj  32843  neldifpr2  33178  xrge0adddir  33626  slmdlema  33811  lmodslmd  33812  fldgensdrg  33923  rhmimaidl  34029  irngnzply1lem  34369  xrge0iifcnv  34612  xrge0iifiso  34614  xrge0iifhom  34616  rrextcusp  34684  rrextust  34687  unelros  34851  difelros  34852  inelsros  34858  diffiunisros  34859  sibfinima  35018  eulerpartlemf  35049  eulerpartlemgvv  35055  bnj563  35421  bnj1366  35506  bnj1379  35507  bnj554  35576  bnj557  35578  bnj570  35582  bnj594  35589  bnj1001  35636  bnj1006  35637  bnj1097  35658  bnj1177  35683  bnj1388  35710  bnj1398  35711  bnj1450  35727  bnj1501  35744  bnj1523  35748  snmlflim  36184  msrval  36390  mclsssvlem  36414  mclsind  36422  ptrecube  38632  cntotbnd  38824  heiborlem8  38846  dmnnzd  39103  eqvreltrrel  39710  atlex  40467  kelac1  44159  binomcxplemcvg  45432  binomcxplemnotnn0  45434  dmstructnn  46020  dmstructfi  46021  elixpconstg  46198  fvixp2  46307  stoweidlem39  47143  stoweidlem60  47164  fourierdlem40  47251  fourierdlem78  47288  idomnzd  49537  arweuthinc  50758