![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp3l | GIF version |
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Ref | Expression |
---|---|
simp3l | ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 107 | . 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒) | |
2 | 1 | 3ad2ant3 962 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∧ w3a 920 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: simpl3l 994 simpr3l 1000 simp13l 1054 simp23l 1060 simp33l 1066 issod 4103 tfisi 4357 tfrlem5 5985 tfrlemibxssdm 5998 tfr1onlembxssdm 6014 tfrcllembxssdm 6027 ecopovtrn 6292 ecopovtrng 6295 addassnqg 6711 ltsonq 6727 ltanqg 6729 ltmnqg 6730 addassnq0 6791 mulasssrg 7074 distrsrg 7075 lttrsr 7078 ltsosr 7080 ltasrg 7086 mulextsr1lem 7095 mulextsr1 7096 axmulass 7178 axdistr 7179 lemul1 7837 reapmul1lem 7838 reapmul1 7839 mulcanap 7899 mulcanap2 7900 divassap 7922 divdirap 7929 div11ap 7932 muldivdirap 7939 divcanap5 7946 apmul1 8020 ltdiv1 8090 ltmuldiv 8096 ledivmul 8099 lemuldiv 8103 ltdiv2 8109 lediv2 8113 ltdiv23 8114 lediv23 8115 modqdi 9551 expaddzap 9694 expmulzap 9696 resqrtcl 10141 dvdscmulr 10457 dvdsmulcr 10458 dvdsadd2b 10475 dvdsgcd 10633 rpexp12i 10766 |
Copyright terms: Public domain | W3C validator |