New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  simprbi GIF version

Theorem simprbi 450
 Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simprbi.1 (φ ↔ (ψ χ))
Assertion
Ref Expression
simprbi (φχ)

Proof of Theorem simprbi
StepHypRef Expression
1 simprbi.1 . . 3 (φ ↔ (ψ χ))
21biimpi 186 . 2 (φ → (ψ χ))
32simprd 449 1 (φχ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  sb1  1651  eumo  2244  2eu1  2284  reurmo  2826  pssne  3365  pssn2lp  3370  ssnpss  3372  eldifn  3389  rabsnt  3797  eldifsni  3840  unimax  3925  ssintub  3944  dfnnc2  4395  nnsucelr  4428  ssfin  4470  vfinspsslem1  4550  opeliunxp  4820  opeldm  4910  dmsnopss  5067  fndm  5182  frn  5228  f1ss  5262  forn  5272  f1f1orn  5297  f1orescnv  5301  f1imacnv  5302  fun11iun  5305  tz6.12-2  5346  foelrn  5425  f1fveq  5473  isorel  5489  isoini2  5498  2ndfo  5506  fovcl  5588  weds  5938  ertr  5954  ertrd  5955  en0  6042  enpw1  6062  ncdisjun  6136  nchoicelem8  6296  nchoicelem15  6303  frecxp  6314  dmfrec  6316  fnfreclem2  6318
 Copyright terms: Public domain W3C validator