Theorem simp3bi 1147

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 1088

This theorem is referenced by:  limuni  6397  smores2  8326  ersym  8686  ertr  8689  fvixp  8878  undifixp  8910  fiint  9284  fiintOLD  9285  winalim2  10656  inar1  10735  supmullem1  12160  supmullem2  12161  supmul  12162  eluzle  12813  ico01fl0  13788  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  sin01gt0  16165  divalglem6  16375  gznegcl  16913  gzcjcl  16914  gzaddcl  16915  gzmulcl  16916  gzabssqcl  16919  4sqlem4a  16929  prdsbasprj  17442  xpsff1o  17537  mreintcl  17563  drsdir  18270  subggrp  19068  pmtrfconj  19403  symggen  19407  psgnunilem1  19430  subgpgp  19534  slwispgp  19548  sylow2alem1  19554  oppglsm  19579  efgsdmi  19669  efgsrel  19671  efgsp1  19674  efgsres  19675  efgcpbllemb  19692  efgcpbl  19693  srgdilem  20108  srgrz  20123  srglz  20124  ringdilem  20165  isringrng  20203  ringsrg  20213  irredmul  20345  subrngss  20464  sdrgdrng  20706  fldsdrgfld  20714  sdrgint  20720  primefld  20721  lmodlema  20778  lsscl  20855  phllmhm  21548  ipcj  21550  ipeq0  21554  ocvi  21585  obsip  21637  obsocv  21642  2ndcctbss  23349  locfinnei  23417  fclssscls  23912  tmdcn  23977  tgpinv  23979  trgtmd  24059  tdrgunit  24061  ngpds  24499  nrmtngdist  24552  elii1  24838  elii2  24839  icopnfcnv  24847  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  phtpcer  24901  pcoass  24931  clmsubrg  24973  cphnmfval  25099  bnsca  25246  uc1pldg  26061  mon1pldg  26062  sinq12ge0  26424  cosq14gt0  26426  cosq14ge0  26427  cos02pilt1  26442  cosq34lt1  26443  sinord  26450  recosf1o  26451  resinf1o  26452  logrnaddcl  26490  logimul  26530  dvlog2lem  26568  atanf  26797  atanneg  26824  atancj  26827  efiatan  26829  atanlogaddlem  26830  atanlogadd  26831  atanlogsub  26833  efiatan2  26834  2efiatan  26835  ressatans  26851  dvatan  26852  areaf  26878  harmonicubnd  26927  harmonicbnd4  26928  lgamgulmlem2  26947  2sqlem2  27336  2sqlem3  27338  dchrvmasumiflem1  27419  pntpbnd2  27505  f1otrg  28805  f1otrge  28806  brbtwn2  28839  ax5seglem3  28865  axpaschlem  28874  axcontlem7  28904  hstel2  32155  stle1  32161  stj  32171  neldifpr2  32470  xrge0adddir  32966  omndadd  33027  slmdlema  33163  lmodslmd  33164  fldgensdrg  33271  orngmul  33288  rhmimaidl  33410  irngnzply1lem  33692  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  rrextcusp  34002  rrextust  34005  unelros  34168  difelros  34169  inelsros  34175  diffiunisros  34176  sibfinima  34337  eulerpartlemf  34368  eulerpartlemgvv  34374  bnj563  34740  bnj1366  34826  bnj1379  34827  bnj554  34896  bnj557  34898  bnj570  34902  bnj594  34909  bnj1001  34956  bnj1006  34957  bnj1097  34978  bnj1177  35003  bnj1388  35030  bnj1398  35031  bnj1450  35047  bnj1501  35064  bnj1523  35068  pthhashvtx  35122  snmlflim  35326  msrval  35532  mclsssvlem  35556  mclsind  35564  ptrecube  37621  cntotbnd  37797  heiborlem8  37819  dmnnzd  38076  eqvreltrrel  38598  atlex  39316  kelac1  43059  binomcxplemcvg  44350  binomcxplemnotnn0  44352  elixpconstg  45090  fvixp2  45200  stoweidlem39  46044  stoweidlem60  46065  fourierdlem40  46152  fourierdlem78  46189  arweuthinc  49522