Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp3r | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp3r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 | . 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: simpl3r 1022 simpr3r 1028 simp13r 1082 simp23r 1088 simp33r 1094 issod 4211 tfisi 4471 fvun1 5455 f1oiso2 5696 tfrlem5 6179 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 reapmul1 8325 mulcanap 8394 mulcanap2 8395 divassap 8418 divdirap 8425 div11ap 8428 apmul1 8516 ltdiv1 8594 ltmuldiv 8600 ledivmul 8603 lemuldiv 8607 lediv2 8617 ltdiv23 8618 lediv23 8619 xaddass2 9621 xlt2add 9631 modqdi 10133 expaddzap 10305 expmulzap 10307 leisorel 10548 resqrtcl 10769 xrbdtri 11013 dvdsgcd 11627 rpexp12i 11760 psmetlecl 12430 xmetlecl 12463 xblcntrps 12509 xblcntr 12510 |
Copyright terms: Public domain | W3C validator |