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  6379  smores2  8286  ersym  8647  ertr  8650  fvixp  8840  undifixp  8872  fiint  9227  winalim2  10607  inar1  10686  supmullem1  12112  supmullem2  12113  supmul  12114  eluzle  12764  ico01fl0  13739  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  sin01gt0  16115  divalglem6  16325  gznegcl  16863  gzcjcl  16864  gzaddcl  16865  gzmulcl  16866  gzabssqcl  16869  4sqlem4a  16879  prdsbasprj  17392  xpsff1o  17488  mreintcl  17514  drsdir  18225  subggrp  19059  pmtrfconj  19395  symggen  19399  psgnunilem1  19422  subgpgp  19526  slwispgp  19540  sylow2alem1  19546  oppglsm  19571  efgsdmi  19661  efgsrel  19663  efgsp1  19666  efgsres  19667  efgcpbllemb  19684  efgcpbl  19685  omndadd  20057  srgdilem  20127  srgrz  20142  srglz  20143  ringdilem  20184  isringrng  20222  ringsrg  20232  irredmul  20365  subrngss  20481  sdrgdrng  20723  fldsdrgfld  20731  sdrgint  20737  primefld  20738  orngmul  20798  lmodlema  20816  lsscl  20893  phllmhm  21587  ipcj  21589  ipeq0  21593  ocvi  21624  obsip  21676  obsocv  21681  2ndcctbss  23399  locfinnei  23467  fclssscls  23962  tmdcn  24027  tgpinv  24029  trgtmd  24109  tdrgunit  24111  ngpds  24548  nrmtngdist  24601  elii1  24887  elii2  24888  icopnfcnv  24896  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  phtpcer  24950  pcoass  24980  clmsubrg  25022  cphnmfval  25148  bnsca  25295  uc1pldg  26110  mon1pldg  26111  sinq12ge0  26473  cosq14gt0  26475  cosq14ge0  26476  cos02pilt1  26491  cosq34lt1  26492  sinord  26499  recosf1o  26500  resinf1o  26501  logrnaddcl  26539  logimul  26579  dvlog2lem  26617  atanf  26846  atanneg  26873  atancj  26876  efiatan  26878  atanlogaddlem  26879  atanlogadd  26880  atanlogsub  26882  efiatan2  26883  2efiatan  26884  ressatans  26900  dvatan  26901  areaf  26927  harmonicubnd  26976  harmonicbnd4  26977  lgamgulmlem2  26996  2sqlem2  27385  2sqlem3  27387  dchrvmasumiflem1  27468  pntpbnd2  27554  f1otrg  28943  f1otrge  28944  brbtwn2  28978  ax5seglem3  29004  axpaschlem  29013  axcontlem7  29043  hstel2  32294  stle1  32300  stj  32310  neldifpr2  32609  xrge0adddir  33100  slmdlema  33285  lmodslmd  33286  fldgensdrg  33396  rhmimaidl  33513  irngnzply1lem  33847  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  rrextcusp  34162  rrextust  34165  unelros  34328  difelros  34329  inelsros  34335  diffiunisros  34336  sibfinima  34496  eulerpartlemf  34527  eulerpartlemgvv  34533  bnj563  34899  bnj1366  34985  bnj1379  34986  bnj554  35055  bnj557  35057  bnj570  35061  bnj594  35068  bnj1001  35115  bnj1006  35116  bnj1097  35137  bnj1177  35162  bnj1388  35189  bnj1398  35190  bnj1450  35206  bnj1501  35223  bnj1523  35227  pthhashvtx  35322  snmlflim  35526  msrval  35732  mclsssvlem  35756  mclsind  35764  ptrecube  37817  cntotbnd  37993  heiborlem8  38015  dmnnzd  38272  eqvreltrrel  38853  atlex  39572  kelac1  43301  binomcxplemcvg  44591  binomcxplemnotnn0  44593  elixpconstg  45329  fvixp2  45439  stoweidlem39  46279  stoweidlem60  46300  fourierdlem40  46387  fourierdlem78  46424  arweuthinc  49770