Theorem simp3bi 1145

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  limuni  6311  smores2  8156  ersym  8468  ertr  8471  fvixp  8648  undifixp  8680  fiint  9021  winalim2  10383  inar1  10462  supmullem1  11875  supmullem2  11876  supmul  11877  eluzle  12524  ico01fl0  13467  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  sin01gt0  15827  divalglem6  16035  gznegcl  16564  gzcjcl  16565  gzaddcl  16566  gzmulcl  16567  gzabssqcl  16570  4sqlem4a  16580  prdsbasprj  17100  xpsff1o  17195  mreintcl  17221  drsdir  17935  subggrp  18673  pmtrfconj  18989  symggen  18993  psgnunilem1  19016  subgpgp  19117  slwispgp  19131  sylow2alem1  19137  oppglsm  19162  efgsdmi  19253  efgsrel  19255  efgsp1  19258  efgsres  19259  efgcpbllemb  19276  efgcpbl  19277  srgi  19662  srgrz  19677  srglz  19678  ringi  19714  ringsrg  19743  irredmul  19866  sdrgint  19987  primefld  19988  lmodlema  20043  lsscl  20119  phllmhm  20749  ipcj  20751  ipeq0  20755  ocvi  20786  obsip  20838  obsocv  20843  2ndcctbss  22514  locfinnei  22582  fclssscls  23077  tmdcn  23142  tgpinv  23144  trgtmd  23224  tdrgunit  23226  ngpds  23666  nrmtngdist  23727  elii1  24004  elii2  24005  icopnfcnv  24011  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  phtpcer  24064  pcoass  24093  clmsubrg  24135  cphnmfval  24261  bnsca  24408  uc1pldg  25218  mon1pldg  25219  sinq12ge0  25570  cosq14gt0  25572  cosq14ge0  25573  cos02pilt1  25587  cosq34lt1  25588  sinord  25595  recosf1o  25596  resinf1o  25597  logrnaddcl  25635  logimul  25674  dvlog2lem  25712  atanf  25935  atanneg  25962  atancj  25965  efiatan  25967  atanlogaddlem  25968  atanlogadd  25969  atanlogsub  25971  efiatan2  25972  2efiatan  25973  ressatans  25989  dvatan  25990  areaf  26016  harmonicubnd  26064  harmonicbnd4  26065  lgamgulmlem2  26084  2sqlem2  26471  2sqlem3  26473  dchrvmasumiflem1  26554  pntpbnd2  26640  f1otrg  27136  f1otrge  27137  brbtwn2  27176  ax5seglem3  27202  axpaschlem  27211  axcontlem7  27241  hstel2  30482  stle1  30488  stj  30498  neldifpr2  30783  xrge0adddir  31203  omndadd  31234  slmdlema  31358  lmodslmd  31359  orngmul  31404  rhmimaidl  31511  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhom  31789  rrextcusp  31855  rrextust  31858  unelros  32039  difelros  32040  inelsros  32046  diffiunisros  32047  sibfinima  32206  eulerpartlemf  32237  eulerpartlemgvv  32243  bnj563  32623  bnj1366  32709  bnj1379  32710  bnj554  32779  bnj557  32781  bnj570  32785  bnj594  32792  bnj1001  32839  bnj1006  32840  bnj1097  32861  bnj1177  32886  bnj1388  32913  bnj1398  32914  bnj1450  32930  bnj1501  32947  bnj1523  32951  pthhashvtx  32989  snmlflim  33194  msrval  33400  mclsssvlem  33424  mclsind  33432  ptrecube  35704  cntotbnd  35881  heiborlem8  35903  dmnnzd  36160  eqvreltrrel  36640  atlex  37257  kelac1  40804  binomcxplemcvg  41861  binomcxplemnotnn0  41863  elixpconstg  42528  fvixp2  42627  stoweidlem39  43470  stoweidlem60  43491  fourierdlem40  43578  fourierdlem78  43615  isringrng  45327