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  6414  smores2  8366  ersym  8729  ertr  8732  fvixp  8914  undifixp  8946  fiint  9336  fiintOLD  9337  winalim2  10708  inar1  10787  supmullem1  12210  supmullem2  12211  supmul  12212  eluzle  12863  ico01fl0  13834  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  sin01gt0  16206  divalglem6  16415  gznegcl  16953  gzcjcl  16954  gzaddcl  16955  gzmulcl  16956  gzabssqcl  16959  4sqlem4a  16969  prdsbasprj  17484  xpsff1o  17579  mreintcl  17605  drsdir  18312  subggrp  19110  pmtrfconj  19445  symggen  19449  psgnunilem1  19472  subgpgp  19576  slwispgp  19590  sylow2alem1  19596  oppglsm  19621  efgsdmi  19711  efgsrel  19713  efgsp1  19716  efgsres  19717  efgcpbllemb  19734  efgcpbl  19735  srgdilem  20150  srgrz  20165  srglz  20166  ringdilem  20207  isringrng  20245  ringsrg  20255  irredmul  20387  subrngss  20506  sdrgdrng  20748  fldsdrgfld  20756  sdrgint  20762  primefld  20763  lmodlema  20820  lsscl  20897  phllmhm  21590  ipcj  21592  ipeq0  21596  ocvi  21627  obsip  21679  obsocv  21684  2ndcctbss  23391  locfinnei  23459  fclssscls  23954  tmdcn  24019  tgpinv  24021  trgtmd  24101  tdrgunit  24103  ngpds  24541  nrmtngdist  24594  elii1  24880  elii2  24881  icopnfcnv  24889  icopnfhmeo  24890  iccpnfhmeo  24892  xrhmeo  24893  phtpcer  24943  pcoass  24973  clmsubrg  25015  cphnmfval  25142  bnsca  25289  uc1pldg  26104  mon1pldg  26105  sinq12ge0  26467  cosq14gt0  26469  cosq14ge0  26470  cos02pilt1  26485  cosq34lt1  26486  sinord  26493  recosf1o  26494  resinf1o  26495  logrnaddcl  26533  logimul  26573  dvlog2lem  26611  atanf  26840  atanneg  26867  atancj  26870  efiatan  26872  atanlogaddlem  26873  atanlogadd  26874  atanlogsub  26876  efiatan2  26877  2efiatan  26878  ressatans  26894  dvatan  26895  areaf  26921  harmonicubnd  26970  harmonicbnd4  26971  lgamgulmlem2  26990  2sqlem2  27379  2sqlem3  27381  dchrvmasumiflem1  27462  pntpbnd2  27548  f1otrg  28796  f1otrge  28797  brbtwn2  28830  ax5seglem3  28856  axpaschlem  28865  axcontlem7  28895  hstel2  32146  stle1  32152  stj  32162  neldifpr2  32461  xrge0adddir  32959  omndadd  33020  slmdlema  33146  lmodslmd  33147  fldgensdrg  33254  orngmul  33271  rhmimaidl  33393  irngnzply1lem  33677  xrge0iifcnv  33910  xrge0iifiso  33912  xrge0iifhom  33914  rrextcusp  33982  rrextust  33985  unelros  34148  difelros  34149  inelsros  34155  diffiunisros  34156  sibfinima  34317  eulerpartlemf  34348  eulerpartlemgvv  34354  bnj563  34720  bnj1366  34806  bnj1379  34807  bnj554  34876  bnj557  34878  bnj570  34882  bnj594  34889  bnj1001  34936  bnj1006  34937  bnj1097  34958  bnj1177  34983  bnj1388  35010  bnj1398  35011  bnj1450  35027  bnj1501  35044  bnj1523  35048  pthhashvtx  35096  snmlflim  35300  msrval  35506  mclsssvlem  35530  mclsind  35538  ptrecube  37590  cntotbnd  37766  heiborlem8  37788  dmnnzd  38045  eqvreltrrel  38564  atlex  39280  kelac1  43034  binomcxplemcvg  44326  binomcxplemnotnn0  44328  elixpconstg  45061  fvixp2  45171  stoweidlem39  46016  stoweidlem60  46037  fourierdlem40  46124  fourierdlem78  46161  arweuthinc  49362