![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simprll | GIF version |
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
Ref | Expression |
---|---|
simprll | ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 107 | . 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 5012 fcof1 5454 mpt20 5605 eroveu 6263 addcmpblnq 6619 mulcmpblnq 6620 ordpipqqs 6626 addcmpblnq0 6695 mulcmpblnq0 6696 nnnq0lem1 6698 prarloclemcalc 6754 addlocpr 6788 distrlem4prl 6836 distrlem4pru 6837 ltpopr 6847 addcmpblnr 6978 mulcmpblnrlemg 6979 mulcmpblnr 6980 prsrlem1 6981 ltsrprg 6986 apreap 7754 apreim 7770 divdivdivap 7868 divmuleqap 7872 divadddivap 7882 divsubdivap 7883 ledivdiv 8035 lediv12a 8039 exbtwnz 9337 iseqcaopr 9558 leexp2r 9627 recvguniq 10019 rsqrmo 10051 qredeu 10623 pw2dvdseu 10690 |
Copyright terms: Public domain | W3C validator |