Theorem simp3bi 1153

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  limuni  6379  smores2  8291  ersym  8653  ertr  8656  fvixp  8847  undifixp  8879  fiint  9234  winalim2  10617  inar1  10696  supmullem1  12124  supmullem2  12125  supmul  12126  eluzle  12799  ico01fl0  13776  ef01bndlem  16149  sin01bnd  16150  cos01bnd  16151  sin01gt0  16155  divalglem6  16365  gznegcl  16904  gzcjcl  16905  gzaddcl  16906  gzmulcl  16907  gzabssqcl  16910  4sqlem4a  16920  prdsbasprj  17433  xpsff1o  17529  mreintcl  17555  drsdir  18266  subggrp  19103  pmtrfconj  19439  symggen  19443  psgnunilem1  19466  subgpgp  19570  slwispgp  19584  sylow2alem1  19590  oppglsm  19615  efgsdmi  19705  efgsrel  19707  efgsp1  19710  efgsres  19711  efgcpbllemb  19728  efgcpbl  19729  omndadd  20101  srgdilem  20171  srgrz  20186  srglz  20187  ringdilem  20228  isringrng  20266  ringsrg  20276  irredmul  20407  subrngss  20527  sdrgdrng  20769  fldsdrgfld  20777  sdrgint  20783  primefld  20784  orngmul  20844  lmodlema  20862  lsscl  20939  phllmhm  21614  ipcj  21616  ipeq0  21620  ocvi  21651  obsip  21703  obsocv  21708  2ndcctbss  23445  locfinnei  23513  fclssscls  24008  tmdcn  24073  tgpinv  24075  trgtmd  24155  tdrgunit  24157  ngpds  24594  nrmtngdist  24647  elii1  24927  elii2  24928  icopnfcnv  24934  icopnfhmeo  24935  iccpnfhmeo  24937  xrhmeo  24938  phtpcer  24987  pcoass  25016  clmsubrg  25058  cphnmfval  25184  bnsca  25331  uc1pldg  26139  mon1pldg  26140  sinq12ge0  26497  cosq14gt0  26499  cosq14ge0  26500  cos02pilt1  26515  cosq34lt1  26516  sinord  26523  recosf1o  26524  resinf1o  26525  logrnaddcl  26563  logimul  26603  dvlog2lem  26641  atanf  26869  atanneg  26896  atancj  26899  efiatan  26901  atanlogaddlem  26902  atanlogadd  26903  atanlogsub  26905  efiatan2  26906  2efiatan  26907  ressatans  26923  dvatan  26924  areaf  26950  harmonicubnd  26998  harmonicbnd4  26999  lgamgulmlem2  27018  2sqlem2  27406  2sqlem3  27408  dchrvmasumiflem1  27489  pntpbnd2  27575  f1otrg  28964  f1otrge  28965  brbtwn2  28999  ax5seglem3  29025  axpaschlem  29034  axcontlem7  29064  hstel2  32315  stle1  32321  stj  32331  neldifpr2  32629  xrge0adddir  33104  slmdlema  33291  lmodslmd  33292  fldgensdrg  33405  rhmimaidl  33522  irngnzply1lem  33881  xrge0iifcnv  34124  xrge0iifiso  34126  xrge0iifhom  34128  rrextcusp  34196  rrextust  34199  unelros  34362  difelros  34363  inelsros  34369  diffiunisros  34370  sibfinima  34530  eulerpartlemf  34561  eulerpartlemgvv  34567  bnj563  34933  bnj1366  35018  bnj1379  35019  bnj554  35088  bnj557  35090  bnj570  35094  bnj594  35101  bnj1001  35148  bnj1006  35149  bnj1097  35170  bnj1177  35195  bnj1388  35222  bnj1398  35223  bnj1450  35239  bnj1501  35256  bnj1523  35260  pthhashvtx  35363  snmlflim  35567  msrval  35773  mclsssvlem  35797  mclsind  35805  ptrecube  37994  cntotbnd  38170  heiborlem8  38192  dmnnzd  38449  eqvreltrrel  39058  atlex  39815  kelac1  43515  binomcxplemcvg  44805  binomcxplemnotnn0  44807  elixpconstg  45543  fvixp2  45652  stoweidlem39  46489  stoweidlem60  46510  fourierdlem40  46597  fourierdlem78  46634  arweuthinc  50026