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 473 | 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 5001 fcof1 5443 fliftfun 5456 addcmpblnq 6557 mulcmpblnq 6558 ordpipqqs 6564 enq0tr 6624 addcmpblnq0 6633 mulcmpblnq0 6634 nnnq0lem1 6636 addnq0mo 6637 mulnq0mo 6638 prarloclemcalc 6692 addlocpr 6726 distrlem4prl 6774 distrlem4pru 6775 addcmpblnr 6916 mulcmpblnrlemg 6917 mulcmpblnr 6918 prsrlem1 6919 addsrmo 6920 mulsrmo 6921 ltsrprg 6924 apreap 7687 apreim 7703 divdivdivap 7801 divsubdivap 7816 ledivdiv 7968 lediv12a 7972 qbtwnz 9260 iseqcaopr 9462 leexp2r 9530 recvguniq 9881 rsqrmo 9913 qredeu 10479 pw2dvdseu 10546 |
Copyright terms: Public domain | W3C validator |