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 1015 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 973 |
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 975 |
This theorem is referenced by: simpl3r 1048 simpr3r 1054 simp13r 1108 simp23r 1114 simp33r 1120 issod 4302 tfisi 4569 fvun1 5560 f1oiso2 5804 tfrlem5 6291 tfr1onlembxssdm 6320 tfrcllembxssdm 6333 ecopovtrn 6608 ecopovtrng 6611 addassnqg 7337 ltsonq 7353 ltanqg 7355 ltmnqg 7356 addassnq0 7417 mulasssrg 7713 distrsrg 7714 lttrsr 7717 ltsosr 7719 ltasrg 7725 mulextsr1lem 7735 mulextsr1 7736 axmulass 7828 axdistr 7829 reapmul1 8507 mulcanap 8576 mulcanap2 8577 divassap 8600 divdirap 8607 div11ap 8610 apmul1 8698 ltdiv1 8777 ltmuldiv 8783 ledivmul 8786 lemuldiv 8790 lediv2 8800 ltdiv23 8801 lediv23 8802 xaddass2 9820 xlt2add 9830 modqdi 10341 expaddzap 10513 expmulzap 10515 leisorel 10765 resqrtcl 10986 xrbdtri 11232 dvdsgcd 11960 rpexp12i 12102 pythagtriplem4 12215 pythagtriplem11 12221 pythagtriplem13 12223 pcpremul 12240 pceu 12242 pcqmul 12250 pcqdiv 12254 psmetlecl 13093 xmetlecl 13126 xblcntrps 13172 xblcntr 13173 |
Copyright terms: Public domain | W3C validator |