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

Theorem simplbi 446
 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 186 . 2 (φ → (ψ χ))
32simpld 445 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:  3simpa  952  reurex  2825  eqimss  3323  pssss  3364  eldifi  3388  inss1  3475  ssunsn2  3865  fnfun  5181  ffn  5223  f1f  5258  f1of1  5286  f1ofo  5293  nfvres  5352  ressnop0  5436  isof1o  5488  1stfo  5505  oprabid  5550  brtxp  5783  otelins2  5791  otelins3  5792  oqelins4  5794  weds  5938  ersym  5952  nchoicelem4  6292  nchoicelem8  6296  nchoicelem9  6297  nchoicelem19  6307  fnfreclem3  6319
 Copyright terms: Public domain W3C validator