Theorem simp3bi 1148

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 1145	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  6385  smores2  8294  ersym  8656  ertr  8659  fvixp  8850  undifixp  8882  fiint  9237  winalim2  10619  inar1  10698  supmullem1  12126  supmullem2  12127  supmul  12128  eluzle  12801  ico01fl0  13778  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  sin01gt0  16157  divalglem6  16367  gznegcl  16906  gzcjcl  16907  gzaddcl  16908  gzmulcl  16909  gzabssqcl  16912  4sqlem4a  16922  prdsbasprj  17435  xpsff1o  17531  mreintcl  17557  drsdir  18268  subggrp  19105  pmtrfconj  19441  symggen  19445  psgnunilem1  19468  subgpgp  19572  slwispgp  19586  sylow2alem1  19592  oppglsm  19617  efgsdmi  19707  efgsrel  19709  efgsp1  19712  efgsres  19713  efgcpbllemb  19730  efgcpbl  19731  omndadd  20103  srgdilem  20173  srgrz  20188  srglz  20189  ringdilem  20230  isringrng  20268  ringsrg  20278  irredmul  20409  subrngss  20525  sdrgdrng  20767  fldsdrgfld  20775  sdrgint  20781  primefld  20782  orngmul  20842  lmodlema  20860  lsscl  20937  phllmhm  21612  ipcj  21614  ipeq0  21618  ocvi  21649  obsip  21701  obsocv  21706  2ndcctbss  23420  locfinnei  23488  fclssscls  23983  tmdcn  24048  tgpinv  24050  trgtmd  24130  tdrgunit  24132  ngpds  24569  nrmtngdist  24622  elii1  24902  elii2  24903  icopnfcnv  24909  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  phtpcer  24962  pcoass  24991  clmsubrg  25033  cphnmfval  25159  bnsca  25306  uc1pldg  26114  mon1pldg  26115  sinq12ge0  26472  cosq14gt0  26474  cosq14ge0  26475  cos02pilt1  26490  cosq34lt1  26491  sinord  26498  recosf1o  26499  resinf1o  26500  logrnaddcl  26538  logimul  26578  dvlog2lem  26616  atanf  26844  atanneg  26871  atancj  26874  efiatan  26876  atanlogaddlem  26877  atanlogadd  26878  atanlogsub  26880  efiatan2  26881  2efiatan  26882  ressatans  26898  dvatan  26899  areaf  26925  harmonicubnd  26973  harmonicbnd4  26974  lgamgulmlem2  26993  2sqlem2  27381  2sqlem3  27383  dchrvmasumiflem1  27464  pntpbnd2  27550  f1otrg  28939  f1otrge  28940  brbtwn2  28974  ax5seglem3  29000  axpaschlem  29009  axcontlem7  29039  hstel2  32290  stle1  32296  stj  32306  neldifpr2  32604  xrge0adddir  33078  slmdlema  33264  lmodslmd  33265  fldgensdrg  33375  rhmimaidl  33492  irngnzply1lem  33834  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  rrextcusp  34149  rrextust  34152  unelros  34315  difelros  34316  inelsros  34322  diffiunisros  34323  sibfinima  34483  eulerpartlemf  34514  eulerpartlemgvv  34520  bnj563  34886  bnj1366  34971  bnj1379  34972  bnj554  35041  bnj557  35043  bnj570  35047  bnj594  35054  bnj1001  35101  bnj1006  35102  bnj1097  35123  bnj1177  35148  bnj1388  35175  bnj1398  35176  bnj1450  35192  bnj1501  35209  bnj1523  35213  pthhashvtx  35310  snmlflim  35514  msrval  35720  mclsssvlem  35744  mclsind  35752  ptrecube  37941  cntotbnd  38117  heiborlem8  38139  dmnnzd  38396  eqvreltrrel  39005  atlex  39762  kelac1  43491  binomcxplemcvg  44781  binomcxplemnotnn0  44783  elixpconstg  45519  fvixp2  45628  stoweidlem39  46467  stoweidlem60  46488  fourierdlem40  46575  fourierdlem78  46612  arweuthinc  50004