Theorem simp3bi 1144

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 1141	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  limuni  6219  smores2  7974  ersym  8284  ertr  8287  fvixp  8449  undifixp  8481  fiint  8779  winalim2  10107  inar1  10186  supmullem1  11598  supmullem2  11599  supmul  11600  eluzle  12244  ico01fl0  13184  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  sin01gt0  15535  divalglem6  15739  gznegcl  16261  gzcjcl  16262  gzaddcl  16263  gzmulcl  16264  gzabssqcl  16267  4sqlem4a  16277  prdsbasprj  16737  xpsff1o  16832  mreintcl  16858  drsdir  17537  subggrp  18274  pmtrfconj  18586  symggen  18590  psgnunilem1  18613  subgpgp  18714  slwispgp  18728  sylow2alem1  18734  oppglsm  18759  efgsdmi  18850  efgsrel  18852  efgsp1  18855  efgsres  18856  efgcpbllemb  18873  efgcpbl  18874  srgi  19254  srgrz  19269  srglz  19270  ringi  19306  ringsrg  19335  irredmul  19455  sdrgint  19576  primefld  19577  lmodlema  19632  lsscl  19707  phllmhm  20321  ipcj  20323  ipeq0  20327  ocvi  20358  obsip  20410  obsocv  20415  2ndcctbss  22060  locfinnei  22128  fclssscls  22623  tmdcn  22688  tgpinv  22690  trgtmd  22770  tdrgunit  22772  ngpds  23210  nrmtngdist  23263  elii1  23540  elii2  23541  icopnfcnv  23547  icopnfhmeo  23548  iccpnfhmeo  23550  xrhmeo  23551  phtpcer  23600  pcoass  23629  clmsubrg  23671  cphnmfval  23797  bnsca  23943  uc1pldg  24749  mon1pldg  24750  sinq12ge0  25101  cosq14gt0  25103  cosq14ge0  25104  cos02pilt1  25118  cosq34lt1  25119  sinord  25126  recosf1o  25127  resinf1o  25128  logrnaddcl  25166  logimul  25205  dvlog2lem  25243  atanf  25466  atanneg  25493  atancj  25496  efiatan  25498  atanlogaddlem  25499  atanlogadd  25500  atanlogsub  25502  efiatan2  25503  2efiatan  25504  ressatans  25520  dvatan  25521  areaf  25547  harmonicubnd  25595  harmonicbnd4  25596  lgamgulmlem2  25615  2sqlem2  26002  2sqlem3  26004  dchrvmasumiflem1  26085  pntpbnd2  26171  f1otrg  26665  f1otrge  26666  brbtwn2  26699  ax5seglem3  26725  axpaschlem  26734  axcontlem7  26764  hstel2  30002  stle1  30008  stj  30018  neldifpr2  30306  xrge0adddir  30726  omndadd  30757  slmdlema  30881  lmodslmd  30882  orngmul  30927  rhmimaidl  31017  xrge0iifcnv  31286  xrge0iifiso  31288  xrge0iifhom  31290  rrextcusp  31356  rrextust  31359  unelros  31540  difelros  31541  inelsros  31547  diffiunisros  31548  sibfinima  31707  eulerpartlemf  31738  eulerpartlemgvv  31744  bnj563  32124  bnj1366  32211  bnj1379  32212  bnj554  32281  bnj557  32283  bnj570  32287  bnj594  32294  bnj1001  32341  bnj1006  32342  bnj1097  32363  bnj1177  32388  bnj1388  32415  bnj1398  32416  bnj1450  32432  bnj1501  32449  bnj1523  32453  pthhashvtx  32487  snmlflim  32692  msrval  32898  mclsssvlem  32922  mclsind  32930  ptrecube  35057  cntotbnd  35234  heiborlem8  35256  dmnnzd  35513  eqvreltrrel  35995  atlex  36612  kelac1  40007  binomcxplemcvg  41058  binomcxplemnotnn0  41060  elixpconstg  41725  fvixp2  41827  stoweidlem39  42681  stoweidlem60  42702  fourierdlem40  42789  fourierdlem78  42826  isringrng  44505