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 1004 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 962 |
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 964 |
This theorem is referenced by: simpl3r 1037 simpr3r 1043 simp13r 1097 simp23r 1103 simp33r 1109 issod 4241 tfisi 4501 fvun1 5487 f1oiso2 5728 tfrlem5 6211 tfr1onlembxssdm 6240 tfrcllembxssdm 6253 ecopovtrn 6526 ecopovtrng 6529 addassnqg 7190 ltsonq 7206 ltanqg 7208 ltmnqg 7209 addassnq0 7270 mulasssrg 7566 distrsrg 7567 lttrsr 7570 ltsosr 7572 ltasrg 7578 mulextsr1lem 7588 mulextsr1 7589 axmulass 7681 axdistr 7682 reapmul1 8357 mulcanap 8426 mulcanap2 8427 divassap 8450 divdirap 8457 div11ap 8460 apmul1 8548 ltdiv1 8626 ltmuldiv 8632 ledivmul 8635 lemuldiv 8639 lediv2 8649 ltdiv23 8650 lediv23 8651 xaddass2 9653 xlt2add 9663 modqdi 10165 expaddzap 10337 expmulzap 10339 leisorel 10580 resqrtcl 10801 xrbdtri 11045 dvdsgcd 11700 rpexp12i 11833 psmetlecl 12503 xmetlecl 12536 xblcntrps 12582 xblcntr 12583 |
Copyright terms: Public domain | W3C validator |