New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > simpl | Unicode 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 2746 r19.40 2762 rr19.28v 2981 eueq3 3011 reu6 3025 sbc2iegf 3112 sbcralt 3118 rmob 3134 csbiebt 3172 ssab2 3350 uneqin 3506 undif3 3515 ifan 3701 difsn 3845 unissel 3920 ssmin 3945 unissint 3950 uniintsn 3963 iota4an 4358 iota2 4367 reiota2 4368 peano1 4402 nnsucelr 4428 ltfintr 4459 ncfineleq 4477 eqtfinrelk 4486 sfinltfin 4535 ncvspfin 4538 vfinspsslem1 4550 phi11lem1 4595 mosubopt 4612 opabssxp 4837 ideqg2 4869 dmcoss 4971 xpcan2 5058 dfxp2 5113 fun11uni 5162 fnbr 5185 fvopab3ig 5387 ffnfv 5427 ffvresb 5431 isomin 5496 f1oiso 5499 fnoprabg 5585 ovmpt2x 5712 fvfullfunlem2 5862 erth 5968 erdisj 5972 ecelqsdm 5994 elnc 6125 pw1fin 6169 dflec3 6221 nchoicelem6 6294 nchoicelem8 6296 |
Copyright terms: Public domain | W3C validator |