![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simprlr | GIF version |
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Ref | Expression |
---|---|
simprlr | ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | ad2antrl 475 | 1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
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 is referenced by: imain 5130 fcof1 5600 fliftfun 5613 sbthlemi6 6751 sbthlemi8 6753 addcmpblnq 7023 mulcmpblnq 7024 ordpipqqs 7030 enq0tr 7090 addcmpblnq0 7099 mulcmpblnq0 7100 nnnq0lem1 7102 addnq0mo 7103 mulnq0mo 7104 prarloclemcalc 7158 addlocpr 7192 distrlem4prl 7240 distrlem4pru 7241 addcmpblnr 7382 mulcmpblnrlemg 7383 mulcmpblnr 7384 prsrlem1 7385 addsrmo 7386 mulsrmo 7387 ltsrprg 7390 apreap 8161 apreim 8177 divdivdivap 8277 divsubdivap 8292 ledivdiv 8448 lediv12a 8452 exbtwnz 9811 seq3caopr 10049 leexp2r 10140 zfz1iso 10377 recvguniq 10559 rsqrmo 10591 summodclem2 10940 qredeu 11521 pw2dvdseu 11588 epttop 11957 metequiv2 12297 |
Copyright terms: Public domain | W3C validator |