Theorem simp3bi 1145

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  limuni  6424  smores2  8368  ersym  8730  ertr  8733  fvixp  8914  undifixp  8946  fiint  9342  winalim2  10713  inar1  10792  supmullem1  12208  supmullem2  12209  supmul  12210  eluzle  12859  ico01fl0  13810  ef01bndlem  16154  sin01bnd  16155  cos01bnd  16156  sin01gt0  16160  divalglem6  16368  gznegcl  16897  gzcjcl  16898  gzaddcl  16899  gzmulcl  16900  gzabssqcl  16903  4sqlem4a  16913  prdsbasprj  17447  xpsff1o  17542  mreintcl  17568  drsdir  18287  subggrp  19077  pmtrfconj  19414  symggen  19418  psgnunilem1  19441  subgpgp  19545  slwispgp  19559  sylow2alem1  19565  oppglsm  19590  efgsdmi  19680  efgsrel  19682  efgsp1  19685  efgsres  19686  efgcpbllemb  19703  efgcpbl  19704  srgdilem  20125  srgrz  20140  srglz  20141  ringdilem  20182  isringrng  20216  ringsrg  20226  irredmul  20361  subrngss  20478  sdrgdrng  20671  fldsdrgfld  20679  sdrgint  20685  primefld  20686  lmodlema  20741  lsscl  20819  phllmhm  21557  ipcj  21559  ipeq0  21563  ocvi  21594  obsip  21648  obsocv  21653  2ndcctbss  23352  locfinnei  23420  fclssscls  23915  tmdcn  23980  tgpinv  23982  trgtmd  24062  tdrgunit  24064  ngpds  24506  nrmtngdist  24567  elii1  24851  elii2  24852  icopnfcnv  24860  icopnfhmeo  24861  iccpnfhmeo  24863  xrhmeo  24864  phtpcer  24914  pcoass  24944  clmsubrg  24986  cphnmfval  25113  bnsca  25260  uc1pldg  26077  mon1pldg  26078  sinq12ge0  26436  cosq14gt0  26438  cosq14ge0  26439  cos02pilt1  26453  cosq34lt1  26454  sinord  26461  recosf1o  26462  resinf1o  26463  logrnaddcl  26501  logimul  26541  dvlog2lem  26579  atanf  26805  atanneg  26832  atancj  26835  efiatan  26837  atanlogaddlem  26838  atanlogadd  26839  atanlogsub  26841  efiatan2  26842  2efiatan  26843  ressatans  26859  dvatan  26860  areaf  26886  harmonicubnd  26935  harmonicbnd4  26936  lgamgulmlem2  26955  2sqlem2  27344  2sqlem3  27346  dchrvmasumiflem1  27427  pntpbnd2  27513  f1otrg  28668  f1otrge  28669  brbtwn2  28709  ax5seglem3  28735  axpaschlem  28744  axcontlem7  28774  hstel2  32022  stle1  32028  stj  32038  neldifpr2  32323  xrge0adddir  32742  omndadd  32780  slmdlema  32904  lmodslmd  32905  fldgensdrg  32995  orngmul  33012  rhmimaidl  33142  irngnzply1lem  33358  xrge0iifcnv  33528  xrge0iifiso  33530  xrge0iifhom  33532  rrextcusp  33600  rrextust  33603  unelros  33784  difelros  33785  inelsros  33791  diffiunisros  33792  sibfinima  33953  eulerpartlemf  33984  eulerpartlemgvv  33990  bnj563  34368  bnj1366  34454  bnj1379  34455  bnj554  34524  bnj557  34526  bnj570  34530  bnj594  34537  bnj1001  34584  bnj1006  34585  bnj1097  34606  bnj1177  34631  bnj1388  34658  bnj1398  34659  bnj1450  34675  bnj1501  34692  bnj1523  34696  pthhashvtx  34731  snmlflim  34936  msrval  35142  mclsssvlem  35166  mclsind  35174  ptrecube  37087  cntotbnd  37263  heiborlem8  37285  dmnnzd  37542  eqvreltrrel  38066  atlex  38782  kelac1  42481  binomcxplemcvg  43785  binomcxplemnotnn0  43787  elixpconstg  44449  fvixp2  44566  stoweidlem39  45421  stoweidlem60  45442  fourierdlem40  45529  fourierdlem78  45566

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »