Theorem simp3bi 1143

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  limuni  6253  smores2  7993  ersym  8303  ertr  8306  fvixp  8468  undifixp  8500  fiint  8797  winalim2  10120  inar1  10199  supmullem1  11613  supmullem2  11614  supmul  11615  eluzle  12259  ico01fl0  13192  ef01bndlem  15539  sin01bnd  15540  cos01bnd  15541  sin01gt0  15545  divalglem6  15751  gznegcl  16273  gzcjcl  16274  gzaddcl  16275  gzmulcl  16276  gzabssqcl  16279  4sqlem4a  16289  prdsbasprj  16747  xpsff1o  16842  mreintcl  16868  drsdir  17547  subggrp  18284  pmtrfconj  18596  symggen  18600  psgnunilem1  18623  subgpgp  18724  slwispgp  18738  sylow2alem1  18744  oppglsm  18769  efgsdmi  18860  efgsrel  18862  efgsp1  18865  efgsres  18866  efgcpbllemb  18883  efgcpbl  18884  srgi  19263  srgrz  19278  srglz  19279  ringi  19312  ringsrg  19341  irredmul  19461  sdrgint  19585  primefld  19586  lmodlema  19641  lsscl  19716  phllmhm  20778  ipcj  20780  ipeq0  20784  ocvi  20815  obsip  20867  obsocv  20872  2ndcctbss  22065  locfinnei  22133  fclssscls  22628  tmdcn  22693  tgpinv  22695  trgtmd  22775  tdrgunit  22777  ngpds  23215  nrmtngdist  23268  elii1  23541  elii2  23542  icopnfcnv  23548  icopnfhmeo  23549  iccpnfhmeo  23551  xrhmeo  23552  phtpcer  23601  pcoass  23630  clmsubrg  23672  cphnmfval  23798  bnsca  23944  uc1pldg  24744  mon1pldg  24745  sinq12ge0  25096  cosq14gt0  25098  cosq14ge0  25099  cos02pilt1  25113  cosq34lt1  25114  sinord  25120  recosf1o  25121  resinf1o  25122  logrnaddcl  25160  logimul  25199  dvlog2lem  25237  atanf  25460  atanneg  25487  atancj  25490  efiatan  25492  atanlogaddlem  25493  atanlogadd  25494  atanlogsub  25496  efiatan2  25497  2efiatan  25498  ressatans  25514  dvatan  25515  areaf  25541  harmonicubnd  25589  harmonicbnd4  25590  lgamgulmlem2  25609  2sqlem2  25996  2sqlem3  25998  dchrvmasumiflem1  26079  pntpbnd2  26165  f1otrg  26659  f1otrge  26660  brbtwn2  26693  ax5seglem3  26719  axpaschlem  26728  axcontlem7  26758  hstel2  29998  stle1  30004  stj  30014  neldifpr2  30296  xrge0adddir  30681  omndadd  30709  slmdlema  30833  lmodslmd  30834  orngmul  30878  xrge0iifcnv  31178  xrge0iifiso  31180  xrge0iifhom  31182  rrextcusp  31248  rrextust  31251  unelros  31432  difelros  31433  inelsros  31439  diffiunisros  31440  sibfinima  31599  eulerpartlemf  31630  eulerpartlemgvv  31636  bnj563  32016  bnj1366  32103  bnj1379  32104  bnj554  32173  bnj557  32175  bnj570  32179  bnj594  32186  bnj1001  32233  bnj1006  32234  bnj1097  32255  bnj1177  32280  bnj1388  32307  bnj1398  32308  bnj1450  32324  bnj1501  32341  bnj1523  32345  pthhashvtx  32376  snmlflim  32581  msrval  32787  mclsssvlem  32811  mclsind  32819  ptrecube  34894  cntotbnd  35076  heiborlem8  35098  dmnnzd  35355  eqvreltrrel  35837  atlex  36454  kelac1  39670  binomcxplemcvg  40693  binomcxplemnotnn0  40695  elixpconstg  41362  fvixp2  41468  stoweidlem39  42331  stoweidlem60  42352  fourierdlem40  42439  fourierdlem78  42476  isringrng  44159