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 1086

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 1088

This theorem is referenced by:  limuni  6368  smores2  8274  ersym  8634  ertr  8637  fvixp  8826  undifixp  8858  fiint  9211  winalim2  10584  inar1  10663  supmullem1  12089  supmullem2  12090  supmul  12091  eluzle  12742  ico01fl0  13720  ef01bndlem  16090  sin01bnd  16091  cos01bnd  16092  sin01gt0  16096  divalglem6  16306  gznegcl  16844  gzcjcl  16845  gzaddcl  16846  gzmulcl  16847  gzabssqcl  16850  4sqlem4a  16860  prdsbasprj  17373  xpsff1o  17468  mreintcl  17494  drsdir  18205  subggrp  19039  pmtrfconj  19376  symggen  19380  psgnunilem1  19403  subgpgp  19507  slwispgp  19521  sylow2alem1  19527  oppglsm  19552  efgsdmi  19642  efgsrel  19644  efgsp1  19647  efgsres  19648  efgcpbllemb  19665  efgcpbl  19666  omndadd  20038  srgdilem  20108  srgrz  20123  srglz  20124  ringdilem  20165  isringrng  20203  ringsrg  20213  irredmul  20345  subrngss  20461  sdrgdrng  20703  fldsdrgfld  20711  sdrgint  20717  primefld  20718  orngmul  20778  lmodlema  20796  lsscl  20873  phllmhm  21567  ipcj  21569  ipeq0  21573  ocvi  21604  obsip  21656  obsocv  21661  2ndcctbss  23368  locfinnei  23436  fclssscls  23931  tmdcn  23996  tgpinv  23998  trgtmd  24078  tdrgunit  24080  ngpds  24517  nrmtngdist  24570  elii1  24856  elii2  24857  icopnfcnv  24865  icopnfhmeo  24866  iccpnfhmeo  24868  xrhmeo  24869  phtpcer  24919  pcoass  24949  clmsubrg  24991  cphnmfval  25117  bnsca  25264  uc1pldg  26079  mon1pldg  26080  sinq12ge0  26442  cosq14gt0  26444  cosq14ge0  26445  cos02pilt1  26460  cosq34lt1  26461  sinord  26468  recosf1o  26469  resinf1o  26470  logrnaddcl  26508  logimul  26548  dvlog2lem  26586  atanf  26815  atanneg  26842  atancj  26845  efiatan  26847  atanlogaddlem  26848  atanlogadd  26849  atanlogsub  26851  efiatan2  26852  2efiatan  26853  ressatans  26869  dvatan  26870  areaf  26896  harmonicubnd  26945  harmonicbnd4  26946  lgamgulmlem2  26965  2sqlem2  27354  2sqlem3  27356  dchrvmasumiflem1  27437  pntpbnd2  27523  f1otrg  28847  f1otrge  28848  brbtwn2  28881  ax5seglem3  28907  axpaschlem  28916  axcontlem7  28946  hstel2  32194  stle1  32200  stj  32210  neldifpr2  32509  xrge0adddir  32994  slmdlema  33167  lmodslmd  33168  fldgensdrg  33275  rhmimaidl  33392  irngnzply1lem  33698  xrge0iifcnv  33941  xrge0iifiso  33943  xrge0iifhom  33945  rrextcusp  34013  rrextust  34016  unelros  34179  difelros  34180  inelsros  34186  diffiunisros  34187  sibfinima  34347  eulerpartlemf  34378  eulerpartlemgvv  34384  bnj563  34750  bnj1366  34836  bnj1379  34837  bnj554  34906  bnj557  34908  bnj570  34912  bnj594  34919  bnj1001  34966  bnj1006  34967  bnj1097  34988  bnj1177  35013  bnj1388  35040  bnj1398  35041  bnj1450  35057  bnj1501  35074  bnj1523  35078  pthhashvtx  35160  snmlflim  35364  msrval  35570  mclsssvlem  35594  mclsind  35602  ptrecube  37659  cntotbnd  37835  heiborlem8  37857  dmnnzd  38114  eqvreltrrel  38636  atlex  39354  kelac1  43095  binomcxplemcvg  44386  binomcxplemnotnn0  44388  elixpconstg  45125  fvixp2  45235  stoweidlem39  46076  stoweidlem60  46097  fourierdlem40  46184  fourierdlem78  46221  arweuthinc  49560