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

Theorem simplbi 272
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 119 . 2 (𝜑 → (𝜓𝜒))
32simpld 111 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.62dc  934  3simpa  983  xoror  1368  anxordi  1389  sbidm  1838  reurex  2677  eqimss  3194  eldifi  3242  elinel1  3306  inss1  3340  sopo  4288  wefr  4333  ordtr  4353  opelxp1  4635  relop  4751  funmo  5200  funrel  5202  funinsn  5234  fnfun  5282  ffn  5334  f1f  5390  f1of1  5428  f1ofo  5436  isof1o  5772  eqopi  6135  1st2nd2  6138  reldmtpos  6215  swoer  6523  ecopover  6593  ecopoverg  6596  fnfi  6896  casef  7047  nninff  7081  lpowlpo  7126  dfplpq2  7289  enq0ref  7368  cauappcvgprlemopl  7581  cauappcvgprlemdisj  7586  caucvgprlemopl  7604  caucvgprlemdisj  7609  caucvgprprlemopl  7632  caucvgprprlemopu  7634  caucvgprprlemdisj  7637  peano1nnnn  7787  axrnegex  7814  ltxrlt  7958  1nn  8862  zre  9189  nnssz  9202  ixxss1  9834  ixxss2  9835  ixxss12  9836  iccss2  9874  rge0ssre  9907  elfzuz  9950  uzdisj  10022  nn0disj  10067  frecuzrdgtcl  10341  frecuzrdgfunlem  10348  modfsummodlemstep  11392  mertenslem2  11471  prmnn  12036  prmuz2  12057  oddpwdc  12100  sqpweven  12101  2sqpwodd  12102  phimullem  12151  hashgcdlem  12164  1arith  12291  ctinfom  12355  ctinf  12357  topontop  12610  tpstop  12631  cntop1  12799  cntop2  12800  hmeocn  12903  isxmet2d  12946  metxmet  12953  xmstps  13055  msxms  13056  xmsxmet  13058  msmet  13059  bdxmet  13099  ivthinclemlr  13213  ivthinclemur  13215  bj-indint  13706  bj-inf2vnlem2  13746  peano4nninf  13779
  Copyright terms: Public domain W3C validator