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 989 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 947 |
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 949 |
This theorem is referenced by: simpl3l 1021 simpr3l 1027 simp13l 1081 simp23l 1087 simp33l 1093 issod 4211 tfisi 4471 tfrlem5 6179 tfrlemibxssdm 6192 tfr1onlembxssdm 6208 tfrcllembxssdm 6221 ecopovtrn 6494 ecopovtrng 6497 addassnqg 7158 ltsonq 7174 ltanqg 7176 ltmnqg 7177 addassnq0 7238 mulasssrg 7534 distrsrg 7535 lttrsr 7538 ltsosr 7540 ltasrg 7546 mulextsr1lem 7556 mulextsr1 7557 axmulass 7649 axdistr 7650 lemul1 8323 reapmul1lem 8324 reapmul1 8325 mulcanap 8394 mulcanap2 8395 divassap 8418 divdirap 8425 div11ap 8428 muldivdirap 8435 divcanap5 8442 apmul1 8516 apmul2 8517 ltdiv1 8594 ltmuldiv 8600 ledivmul 8603 lemuldiv 8607 ltdiv2 8613 lediv2 8617 ltdiv23 8618 lediv23 8619 xaddass2 9621 xlt2add 9631 modqdi 10133 expaddzap 10305 expmulzap 10307 leisorel 10548 resqrtcl 10769 xrbdtri 11013 dvdscmulr 11449 dvdsmulcr 11450 dvdsadd2b 11467 dvdsgcd 11627 rpexp12i 11760 psmetlecl 12430 xmetlecl 12463 |
Copyright terms: Public domain | W3C validator |