Theorem simp1bi 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
simp1bi	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 216	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp1d 1142	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:  limord  6367  smores2  8274  smofvon2  8276  smofvon  8279  errel  8631  elunitrn  13367  lincmb01cmp  13395  iccf1o  13396  elfznn0  13520  elfzouz  13563  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  sin01gt0  16099  cos01gt0  16100  sin02gt0  16101  gzcn  16844  mresspw  17494  drsprs  18209  ipodrscl  18444  subgrcl  19044  pmtrfconj  19379  pgpprm  19506  slwprm  19522  efgsdmi  19645  efgsrel  19647  efgs1b  19649  efgsp1  19650  efgsres  19651  efgsfo  19652  efgredlema  19653  efgredlemf  19654  efgredlemd  19657  efgredlemc  19658  efgredlem  19660  efgrelexlemb  19663  efgcpbllemb  19668  omndmnd  20039  rngabl  20074  srgcmn  20108  ringgrp  20157  irredcl  20343  subrngrcl  20467  sdrgrcl  20705  orngring  20778  lmodgrp  20801  lssss  20870  phllvec  21567  obsrcl  21661  locfintop  23437  fclstop  23927  tmdmnd  23991  tgpgrp  23994  trgtgp  24084  tdrgtrg  24089  ust0  24136  ngpgrp  24515  elii1  24859  elii2  24860  icopnfcnv  24868  icopnfhmeo  24869  iccpnfhmeo  24871  xrhmeo  24872  oprpiece1res2  24878  phtpcer  24922  pcoval2  24944  pcoass  24952  clmlmod  24995  cphphl  25099  cphnlm  25100  cphsca  25107  bnnvc  25268  uc1pcl  26077  mon1pcl  26078  sinq12ge0  26445  cosq14ge0  26448  cosq34lt1  26464  cosord  26468  cos11  26470  recosf1o  26472  resinf1o  26473  efifo  26484  logrncn  26499  atanf  26818  atanneg  26845  efiatan  26850  atanlogaddlem  26851  atanlogadd  26852  atanlogsub  26854  efiatan2  26855  2efiatan  26856  tanatan  26857  areass  26897  dchrvmasumlem2  27437  dchrvmasumiflem1  27440  brbtwn2  28884  ax5seglem1  28907  ax5seglem2  28908  ax5seglem3  28910  ax5seglem5  28912  ax5seglem6  28913  ax5seglem9  28916  ax5seg  28917  axbtwnid  28918  axpaschlem  28919  axpasch  28920  axcontlem2  28944  axcontlem4  28946  axcontlem7  28949  pthistrl  29702  clwwlkbp  29963  sticl  32193  hstcl  32195  slmdcmn  33172  rrextnrg  34012  rrextdrg  34013  rossspw  34180  srossspw  34187  eulerpartlemd  34377  eulerpartlemf  34381  eulerpartlemgvv  34387  eulerpartlemgu  34388  eulerpartlemgh  34389  eulerpartlemgs2  34391  eulerpartlemn  34392  bnj564  34754  bnj1366  34839  bnj545  34905  bnj548  34907  bnj558  34912  bnj570  34915  bnj580  34923  bnj929  34946  bnj998  34967  bnj1006  34970  bnj1190  35018  bnj1523  35081  msrval  35580  mthmpps  35624  eqvrelrefrel  38641  atllat  39345  stoweidlem60  46104  fourierdlem111  46261  modmknepk  47399  prproropf1o  47544  gpgedgvtx1  48099  arweutermc  49568