New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simpl | GIF version |
Description: Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |
Ref | Expression |
---|---|
simpl | ⊢ ((φ ∧ ψ) → φ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 6 | . 2 ⊢ (φ → (ψ → φ)) | |
2 | 1 | imp 418 | 1 ⊢ ((φ ∧ ψ) → φ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: simpli 444 simpld 445 adantrd 454 iba 489 pm3.41 542 pm4.45im 545 prth 554 pm4.44 560 pm4.71 611 adantlr 695 adantrr 697 adantllr 699 adantlrr 701 adantrlr 703 adantrrr 705 simplll 734 simplrl 736 simprll 738 simprrl 740 anabs1 783 jcab 833 pm4.39 841 pm4.38 842 intnanr 881 intnanrd 883 dedlema 920 dedlemb 921 prlem2 929 simp1l 979 simp2l 981 simp3l 983 3anandis 1283 nic-ax 1438 nic-axALT 1439 exsimpl 1592 19.26 1593 sbequ2 1650 mooran1 2258 euan 2261 eupickbi 2270 2eu2 2285 dimatis 2320 r19.26 2747 r19.40 2763 rr19.28v 2982 eueq3 3012 reu6 3026 sbc2iegf 3113 sbcralt 3119 rmob 3135 csbiebt 3173 ssab2 3351 uneqin 3507 undif3 3516 ifan 3702 difsn 3846 unissel 3921 ssmin 3946 unissint 3951 uniintsn 3964 iota4an 4359 iota2 4368 reiota2 4369 peano1 4403 nnsucelr 4429 ltfintr 4460 ncfineleq 4478 eqtfinrelk 4487 sfinltfin 4536 ncvspfin 4539 vfinspsslem1 4551 phi11lem1 4596 mosubopt 4613 opabssxp 4838 ideqg2 4870 dmcoss 4972 xpcan2 5059 dfxp2 5114 fun11uni 5163 fnbr 5186 fvopab3ig 5388 ffnfv 5428 ffvresb 5432 isomin 5497 f1oiso 5500 fnoprabg 5586 ovmpt2x 5713 fvfullfunlem2 5863 erth 5969 erdisj 5973 ecelqsdm 5995 elnc 6126 pw1fin 6170 dflec3 6222 nchoicelem6 6295 nchoicelem8 6297 |
Copyright terms: Public domain | W3C validator |