Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simprrr | GIF version |
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Ref | Expression |
---|---|
simprrr | ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 103 | . 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃) | |
2 | 1 | ad2antll 460 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: fliftfun 5436 grpridd 5697 tfrlemisucaccv 5939 addcmpblnq 6465 mulcmpblnq 6466 ordpipqqs 6472 nqnq0pi 6536 addcmpblnq0 6541 mulcmpblnq0 6542 addnq0mo 6545 mulnq0mo 6546 prarloclemcalc 6600 prarloc 6601 nqprl 6649 mullocpr 6669 distrlem4prl 6682 distrlem4pru 6683 ltprordil 6687 ltexprlemlol 6700 ltexprlemopu 6701 ltexprlemupu 6702 ltexprlemru 6710 cauappcvgprlemopl 6744 cauappcvgprlem2 6758 caucvgprlemopl 6767 caucvgprlem2 6778 caucvgprprlemexbt 6804 caucvgprprlem2 6808 addcmpblnr 6824 mulcmpblnrlemg 6825 mulcmpblnr 6826 prsrlem1 6827 addsrmo 6828 mulsrmo 6829 ltsrprg 6832 axmulcl 6942 recriota 6964 ltmul1 7583 divdivdivap 7689 divsubdivap 7704 ledivdiv 7856 lediv12a 7860 qbtwnz 9106 qbtwnre 9111 iseqcaopr 9242 leexp2r 9308 recvguniq 9593 rsqrmo 9625 |
Copyright terms: Public domain | W3C validator |