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  914  3simpa  963  xoror  1342  anxordi  1363  sbidm  1807  reurex  2621  eqimss  3121  eldifi  3168  elinel1  3232  inss1  3266  sopo  4205  wefr  4250  ordtr  4270  opelxp1  4543  relop  4659  funmo  5108  funrel  5110  funinsn  5142  fnfun  5190  ffn  5242  f1f  5298  f1of1  5334  f1ofo  5342  isof1o  5676  eqopi  6038  1st2nd2  6041  reldmtpos  6118  swoer  6425  ecopover  6495  ecopoverg  6498  fnfi  6793  casef  6941  dfplpq2  7130  enq0ref  7209  cauappcvgprlemopl  7422  cauappcvgprlemdisj  7427  caucvgprlemopl  7445  caucvgprlemdisj  7450  caucvgprprlemopl  7473  caucvgprprlemopu  7475  caucvgprprlemdisj  7478  peano1nnnn  7628  axrnegex  7655  ltxrlt  7798  1nn  8699  zre  9026  nnssz  9039  ixxss1  9655  ixxss2  9656  ixxss12  9657  iccss2  9695  rge0ssre  9728  elfzuz  9770  uzdisj  9841  nn0disj  9883  frecuzrdgtcl  10153  frecuzrdgfunlem  10160  modfsummodlemstep  11194  mertenslem2  11273  prmnn  11718  prmuz2  11738  oddpwdc  11779  sqpweven  11780  2sqpwodd  11781  phimullem  11828  hashgcdlem  11830  ctinfom  11868  ctinf  11870  topontop  12108  tpstop  12129  cntop1  12297  cntop2  12298  hmeocn  12401  isxmet2d  12444  metxmet  12451  xmstps  12553  msxms  12554  xmsxmet  12556  msmet  12557  bdxmet  12597  ivthinclemlr  12711  ivthinclemur  12713  bj-indint  13056  bj-inf2vnlem2  13096  nninff  13125  peano4nninf  13127
  Copyright terms: Public domain W3C validator