ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simplbi GIF version

Theorem simplbi 274
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simplbi.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
simplbi (𝜑𝜓)

Proof of Theorem simplbi
StepHypRef Expression
1 simplbi.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21biimpi 120 . 2 (𝜑 → (𝜓𝜒))
32simpld 112 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm5.62dc  945  3simpa  994  xoror  1379  anxordi  1400  sbidm  1851  reurex  2691  eqimss  3211  eldifi  3259  elinel1  3323  inss1  3357  sopo  4315  wefr  4360  ordtr  4380  opelxp1  4662  relop  4779  funmo  5233  funrel  5235  funinsn  5267  fnfun  5315  ffn  5367  f1f  5423  f1of1  5462  f1ofo  5470  isof1o  5811  eqopi  6176  1st2nd2  6179  reldmtpos  6257  swoer  6566  ecopover  6636  ecopoverg  6639  fnfi  6939  casef  7090  nninff  7124  lpowlpo  7169  dfplpq2  7356  enq0ref  7435  cauappcvgprlemopl  7648  cauappcvgprlemdisj  7653  caucvgprlemopl  7671  caucvgprlemdisj  7676  caucvgprprlemopl  7699  caucvgprprlemopu  7701  caucvgprprlemdisj  7704  peano1nnnn  7854  axrnegex  7881  ltxrlt  8026  1nn  8933  zre  9260  nnssz  9273  ixxss1  9907  ixxss2  9908  ixxss12  9909  iccss2  9947  rge0ssre  9980  elfzuz  10024  uzdisj  10096  nn0disj  10141  frecuzrdgtcl  10415  frecuzrdgfunlem  10422  modfsummodlemstep  11468  mertenslem2  11547  prmnn  12113  prmuz2  12134  oddpwdc  12177  sqpweven  12178  2sqpwodd  12179  phimullem  12228  hashgcdlem  12241  1arith  12368  ctinfom  12432  ctinf  12434  sgrpmgm  12820  mndsgrp  12830  grpmnd  12892  nsgsubg  13079  ablgrp  13108  cmnmnd  13119  crngring  13229  subrgring  13383  subrgrcl  13385  topontop  13702  tpstop  13723  cntop1  13889  cntop2  13890  hmeocn  13993  isxmet2d  14036  metxmet  14043  xmstps  14145  msxms  14146  xmsxmet  14148  msmet  14149  bdxmet  14189  ivthinclemlr  14303  ivthinclemur  14305  bj-indint  14871  bj-inf2vnlem2  14911  peano4nninf  14944
  Copyright terms: Public domain W3C validator