![]() |
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 108 | . 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒) | |
2 | 1 | ad2antrl 474 | 1 ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
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 is referenced by: imain 5032 fcof1 5475 fliftfun 5488 addcmpblnq 6689 mulcmpblnq 6690 ordpipqqs 6696 enq0tr 6756 addcmpblnq0 6765 mulcmpblnq0 6766 nnnq0lem1 6768 addnq0mo 6769 mulnq0mo 6770 prarloclemcalc 6824 addlocpr 6858 distrlem4prl 6906 distrlem4pru 6907 addcmpblnr 7048 mulcmpblnrlemg 7049 mulcmpblnr 7050 prsrlem1 7051 addsrmo 7052 mulsrmo 7053 ltsrprg 7056 apreap 7824 apreim 7840 divdivdivap 7938 divsubdivap 7953 ledivdiv 8105 lediv12a 8109 exbtwnz 9407 iseqcaopr 9628 leexp2r 9697 recvguniq 10100 rsqrmo 10132 qredeu 10704 pw2dvdseu 10771 |
Copyright terms: Public domain | W3C validator |