![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp3r | GIF 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 972 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 930 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 932 |
This theorem is referenced by: simpl3r 1005 simpr3r 1011 simp13r 1065 simp23r 1071 simp33r 1077 issod 4179 tfisi 4439 fvun1 5419 f1oiso2 5660 tfrlem5 6141 tfr1onlembxssdm 6170 tfrcllembxssdm 6183 ecopovtrn 6456 ecopovtrng 6459 addassnqg 7091 ltsonq 7107 ltanqg 7109 ltmnqg 7110 addassnq0 7171 mulasssrg 7454 distrsrg 7455 lttrsr 7458 ltsosr 7460 ltasrg 7466 mulextsr1lem 7475 mulextsr1 7476 axmulass 7558 axdistr 7559 reapmul1 8223 mulcanap 8287 mulcanap2 8288 divassap 8311 divdirap 8318 div11ap 8321 apmul1 8409 ltdiv1 8484 ltmuldiv 8490 ledivmul 8493 lemuldiv 8497 lediv2 8507 ltdiv23 8508 lediv23 8509 xaddass2 9494 xlt2add 9504 modqdi 10006 expaddzap 10178 expmulzap 10180 leisorel 10421 resqrtcl 10641 xrbdtri 10884 dvdsgcd 11493 rpexp12i 11626 psmetlecl 12262 xmetlecl 12295 xblcntrps 12341 xblcntr 12342 |
Copyright terms: Public domain | W3C validator |