![]() |
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 110 | . 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃) | |
2 | 1 | 3ad2ant3 1021 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 981 |
This theorem is referenced by: simpl3r 1054 simpr3r 1060 simp13r 1114 simp23r 1120 simp33r 1126 issod 4333 tfisi 4600 fvun1 5597 f1oiso2 5843 tfrlem5 6332 tfr1onlembxssdm 6361 tfrcllembxssdm 6374 ecopovtrn 6649 ecopovtrng 6652 dftap2 7267 addassnqg 7398 ltsonq 7414 ltanqg 7416 ltmnqg 7417 addassnq0 7478 mulasssrg 7774 distrsrg 7775 lttrsr 7778 ltsosr 7780 ltasrg 7786 mulextsr1lem 7796 mulextsr1 7797 axmulass 7889 axdistr 7890 reapmul1 8569 mulcanap 8639 mulcanap2 8640 divassap 8664 divdirap 8671 div11ap 8674 apmul1 8762 ltdiv1 8842 ltmuldiv 8848 ledivmul 8851 lemuldiv 8855 lediv2 8865 ltdiv23 8866 lediv23 8867 xaddass2 9887 xlt2add 9897 modqdi 10409 expaddzap 10581 expmulzap 10583 leisorel 10834 resqrtcl 11055 xrbdtri 11301 dvdsgcd 12030 rpexp12i 12172 pythagtriplem4 12285 pythagtriplem11 12291 pythagtriplem13 12293 pcpremul 12310 pceu 12312 pcqmul 12320 pcqdiv 12324 f1ocpbllem 12752 ercpbl 12772 erlecpbl 12773 cmn4 13204 ablsub4 13212 abladdsub4 13213 lidlsubcl 13763 psmetlecl 14217 xmetlecl 14250 xblcntrps 14296 xblcntr 14297 |
Copyright terms: Public domain | W3C validator |