Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp3l | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp3l |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 108 | . 2 | |
2 | 1 | 3ad2ant3 1009 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: simpl3l 1041 simpr3l 1047 simp13l 1101 simp23l 1107 simp33l 1113 issod 4291 tfisi 4558 tfrlem5 6273 tfrlemibxssdm 6286 tfr1onlembxssdm 6302 tfrcllembxssdm 6315 ecopovtrn 6589 ecopovtrng 6592 addassnqg 7314 ltsonq 7330 ltanqg 7332 ltmnqg 7333 addassnq0 7394 mulasssrg 7690 distrsrg 7691 lttrsr 7694 ltsosr 7696 ltasrg 7702 mulextsr1lem 7712 mulextsr1 7713 axmulass 7805 axdistr 7806 lemul1 8482 reapmul1lem 8483 reapmul1 8484 mulcanap 8553 mulcanap2 8554 divassap 8577 divdirap 8584 div11ap 8587 muldivdirap 8594 divcanap5 8601 apmul1 8675 apmul2 8676 ltdiv1 8754 ltmuldiv 8760 ledivmul 8763 lemuldiv 8767 ltdiv2 8773 lediv2 8777 ltdiv23 8778 lediv23 8779 xaddass2 9797 xlt2add 9807 modqdi 10317 expaddzap 10489 expmulzap 10491 leisorel 10736 resqrtcl 10957 xrbdtri 11203 dvdscmulr 11746 dvdsmulcr 11747 dvdsadd2b 11765 dvdsgcd 11930 rpexp12i 12066 pythagtriplem3 12178 pcpremul 12204 pceu 12206 pcqmul 12214 pcqdiv 12218 psmetlecl 12881 xmetlecl 12914 |
Copyright terms: Public domain | W3C validator |