Theorem simp3bi 1147

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  limuni  6456  smores2  8410  ersym  8775  ertr  8778  fvixp  8960  undifixp  8992  fiint  9394  fiintOLD  9395  winalim2  10765  inar1  10844  supmullem1  12265  supmullem2  12266  supmul  12267  eluzle  12916  ico01fl0  13870  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  sin01gt0  16238  divalglem6  16446  gznegcl  16982  gzcjcl  16983  gzaddcl  16984  gzmulcl  16985  gzabssqcl  16988  4sqlem4a  16998  prdsbasprj  17532  xpsff1o  17627  mreintcl  17653  drsdir  18372  subggrp  19169  pmtrfconj  19508  symggen  19512  psgnunilem1  19535  subgpgp  19639  slwispgp  19653  sylow2alem1  19659  oppglsm  19684  efgsdmi  19774  efgsrel  19776  efgsp1  19779  efgsres  19780  efgcpbllemb  19797  efgcpbl  19798  srgdilem  20219  srgrz  20234  srglz  20235  ringdilem  20276  isringrng  20310  ringsrg  20320  irredmul  20455  subrngss  20574  sdrgdrng  20813  fldsdrgfld  20821  sdrgint  20827  primefld  20828  lmodlema  20885  lsscl  20963  phllmhm  21673  ipcj  21675  ipeq0  21679  ocvi  21710  obsip  21764  obsocv  21769  2ndcctbss  23484  locfinnei  23552  fclssscls  24047  tmdcn  24112  tgpinv  24114  trgtmd  24194  tdrgunit  24196  ngpds  24638  nrmtngdist  24699  elii1  24983  elii2  24984  icopnfcnv  24992  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  phtpcer  25046  pcoass  25076  clmsubrg  25118  cphnmfval  25245  bnsca  25392  uc1pldg  26208  mon1pldg  26209  sinq12ge0  26568  cosq14gt0  26570  cosq14ge0  26571  cos02pilt1  26586  cosq34lt1  26587  sinord  26594  recosf1o  26595  resinf1o  26596  logrnaddcl  26634  logimul  26674  dvlog2lem  26712  atanf  26941  atanneg  26968  atancj  26971  efiatan  26973  atanlogaddlem  26974  atanlogadd  26975  atanlogsub  26977  efiatan2  26978  2efiatan  26979  ressatans  26995  dvatan  26996  areaf  27022  harmonicubnd  27071  harmonicbnd4  27072  lgamgulmlem2  27091  2sqlem2  27480  2sqlem3  27482  dchrvmasumiflem1  27563  pntpbnd2  27649  f1otrg  28897  f1otrge  28898  brbtwn2  28938  ax5seglem3  28964  axpaschlem  28973  axcontlem7  29003  hstel2  32251  stle1  32257  stj  32267  neldifpr2  32562  xrge0adddir  33004  omndadd  33056  slmdlema  33182  lmodslmd  33183  fldgensdrg  33281  orngmul  33298  rhmimaidl  33425  irngnzply1lem  33690  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  rrextcusp  33951  rrextust  33954  unelros  34135  difelros  34136  inelsros  34142  diffiunisros  34143  sibfinima  34304  eulerpartlemf  34335  eulerpartlemgvv  34341  bnj563  34719  bnj1366  34805  bnj1379  34806  bnj554  34875  bnj557  34877  bnj570  34881  bnj594  34888  bnj1001  34935  bnj1006  34936  bnj1097  34957  bnj1177  34982  bnj1388  35009  bnj1398  35010  bnj1450  35026  bnj1501  35043  bnj1523  35047  pthhashvtx  35095  snmlflim  35300  msrval  35506  mclsssvlem  35530  mclsind  35538  ptrecube  37580  cntotbnd  37756  heiborlem8  37778  dmnnzd  38035  eqvreltrrel  38556  atlex  39272  kelac1  43020  binomcxplemcvg  44323  binomcxplemnotnn0  44325  elixpconstg  44991  fvixp2  45106  stoweidlem39  45960  stoweidlem60  45981  fourierdlem40  46068  fourierdlem78  46105