![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > simplbi | GIF version |
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |
Ref | Expression |
---|---|
simplbi.1 | ⊢ (φ ↔ (ψ ∧ χ)) |
Ref | Expression |
---|---|
simplbi | ⊢ (φ → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplbi.1 | . . 3 ⊢ (φ ↔ (ψ ∧ χ)) | |
2 | 1 | biimpi 186 | . 2 ⊢ (φ → (ψ ∧ χ)) |
3 | 2 | simpld 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 |