P. 10 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 901-1000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3simpb 901	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) -> (ph /\ ch))
Theorem	3simpc 902	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ((ph /\ ps /\ ch) -> (ps /\ ch))
Theorem	simp1 903	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) -> ph)
Theorem	simp2 904	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) -> ps)
Theorem	simp3 905	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) -> ch)
Theorem	simpl1 906	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- (((ph /\ ps /\ ch) /\ th) -> ph)
Theorem	simpl2 907	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- (((ph /\ ps /\ ch) /\ th) -> ps)
Theorem	simpl3 908	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- (((ph /\ ps /\ ch) /\ th) -> ch)
Theorem	simpr1 909	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ((ph /\ (ps /\ ch /\ th)) -> ps)
Theorem	simpr2 910	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ((ph /\ (ps /\ ch /\ th)) -> ch)
Theorem	simpr3 911	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ((ph /\ (ps /\ ch /\ th)) -> th)
Theorem	simp1i 912	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- (ph /\ ps /\ ch)   =>   |- ph
Theorem	simp2i 913	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- (ph /\ ps /\ ch)   =>   |- ps
Theorem	simp3i 914	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- (ph /\ ps /\ ch)   =>   |- ch
Theorem	simp1d 915	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- (ph -> (ps /\ ch /\ th))   =>   |- (ph -> ps)
Theorem	simp2d 916	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- (ph -> (ps /\ ch /\ th))   =>   |- (ph -> ch)
Theorem	simp3d 917	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- (ph -> (ps /\ ch /\ th))   =>   |- (ph -> th)
Theorem	simp1bi 918	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph <-> (ps /\ ch /\ th))   =>   |- (ph -> ps)
Theorem	simp2bi 919	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph <-> (ps /\ ch /\ th))   =>   |- (ph -> ch)
Theorem	simp3bi 920	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph <-> (ps /\ ch /\ th))   =>   |- (ph -> th)
Theorem	3adant1 921	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ((ph /\ ps) -> ch)   =>   |- ((th /\ ph /\ ps) -> ch)
Theorem	3adant2 922	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ((ph /\ ps) -> ch)   =>   |- ((ph /\ th /\ ps) -> ch)
Theorem	3adant3 923	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ((ph /\ ps) -> ch)   =>   |- ((ph /\ ps /\ th) -> ch)
Theorem	3ad2ant1 924	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- (ph -> ch)   =>   |- ((ph /\ ps /\ th) -> ch)
Theorem	3ad2ant2 925	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- (ph -> ch)   =>   |- ((ps /\ ph /\ th) -> ch)
Theorem	3ad2ant3 926	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- (ph -> ch)   =>   |- ((ps /\ th /\ ph) -> ch)
Theorem	simp1l 927	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- (((ph /\ ps) /\ ch /\ th) -> ph)
Theorem	simp1r 928	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- (((ph /\ ps) /\ ch /\ th) -> ps)
Theorem	simp2l 929	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ((ph /\ (ps /\ ch) /\ th) -> ps)
Theorem	simp2r 930	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ((ph /\ (ps /\ ch) /\ th) -> ch)
Theorem	simp3l 931	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th)) -> ch)
Theorem	simp3r 932	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th)) -> th)
Theorem	simp11 933	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- (((ph /\ ps /\ ch) /\ th /\ ta) -> ph)
Theorem	simp12 934	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- (((ph /\ ps /\ ch) /\ th /\ ta) -> ps)
Theorem	simp13 935	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- (((ph /\ ps /\ ch) /\ th /\ ta) -> ch)
Theorem	simp21 936	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ (ps /\ ch /\ th) /\ ta) -> ps)
Theorem	simp22 937	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ (ps /\ ch /\ th) /\ ta) -> ch)
Theorem	simp23 938	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ (ps /\ ch /\ th) /\ ta) -> th)
Theorem	simp31 939	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th /\ ta)) -> ch)
Theorem	simp32 940	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th /\ ta)) -> th)
Theorem	simp33 941	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th /\ ta)) -> ta)
Theorem	simpll1 942	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th) /\ ta) -> ph)
Theorem	simpll2 943	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th) /\ ta) -> ps)
Theorem	simpll3 944	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th) /\ ta) -> ch)
Theorem	simplr1 945	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch)) /\ ta) -> ph)
Theorem	simplr2 946	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch)) /\ ta) -> ps)
Theorem	simplr3 947	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch)) /\ ta) -> ch)
Theorem	simprl1 948	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ ((ph /\ ps /\ ch) /\ th)) -> ph)
Theorem	simprl2 949	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ ((ph /\ ps /\ ch) /\ th)) -> ps)
Theorem	simprl3 950	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ ((ph /\ ps /\ ch) /\ th)) -> ch)
Theorem	simprr1 951	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ (th /\ (ph /\ ps /\ ch))) -> ph)
Theorem	simprr2 952	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ (th /\ (ph /\ ps /\ ch))) -> ps)
Theorem	simprr3 953	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ (th /\ (ph /\ ps /\ ch))) -> ch)
Theorem	simpl1l 954	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps) /\ ch /\ th) /\ ta) -> ph)
Theorem	simpl1r 955	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps) /\ ch /\ th) /\ ta) -> ps)
Theorem	simpl2l 956	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((ch /\ (ph /\ ps) /\ th) /\ ta) -> ph)
Theorem	simpl2r 957	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((ch /\ (ph /\ ps) /\ th) /\ ta) -> ps)
Theorem	simpl3l 958	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((ch /\ th /\ (ph /\ ps)) /\ ta) -> ph)
Theorem	simpl3r 959	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((ch /\ th /\ (ph /\ ps)) /\ ta) -> ps)
Theorem	simpr1l 960	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ ((ph /\ ps) /\ ch /\ th)) -> ph)
Theorem	simpr1r 961	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ ((ph /\ ps) /\ ch /\ th)) -> ps)
Theorem	simpr2l 962	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ (ch /\ (ph /\ ps) /\ th)) -> ph)
Theorem	simpr2r 963	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ (ch /\ (ph /\ ps) /\ th)) -> ps)
Theorem	simpr3l 964	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ (ch /\ th /\ (ph /\ ps))) -> ph)
Theorem	simpr3r 965	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ (ch /\ th /\ (ph /\ ps))) -> ps)
Theorem	simp1ll 966	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps) /\ ch) /\ th /\ ta) -> ph)
Theorem	simp1lr 967	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps) /\ ch) /\ th /\ ta) -> ps)
Theorem	simp1rl 968	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((ch /\ (ph /\ ps)) /\ th /\ ta) -> ph)
Theorem	simp1rr 969	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((ch /\ (ph /\ ps)) /\ th /\ ta) -> ps)
Theorem	simp2ll 970	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((th /\ ((ph /\ ps) /\ ch) /\ ta) -> ph)
Theorem	simp2lr 971	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((th /\ ((ph /\ ps) /\ ch) /\ ta) -> ps)
Theorem	simp2rl 972	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((th /\ (ch /\ (ph /\ ps)) /\ ta) -> ph)
Theorem	simp2rr 973	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((th /\ (ch /\ (ph /\ ps)) /\ ta) -> ps)
Theorem	simp3ll 974	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((th /\ ta /\ ((ph /\ ps) /\ ch)) -> ph)
Theorem	simp3lr 975	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((th /\ ta /\ ((ph /\ ps) /\ ch)) -> ps)
Theorem	simp3rl 976	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((th /\ ta /\ (ch /\ (ph /\ ps))) -> ph)
Theorem	simp3rr 977	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((th /\ ta /\ (ch /\ (ph /\ ps))) -> ps)
Theorem	simpl11 978	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th /\ ta) /\ et) -> ph)
Theorem	simpl12 979	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th /\ ta) /\ et) -> ps)
Theorem	simpl13 980	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th /\ ta) /\ et) -> ch)
Theorem	simpl21 981	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch) /\ ta) /\ et) -> ph)
Theorem	simpl22 982	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch) /\ ta) /\ et) -> ps)
Theorem	simpl23 983	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch) /\ ta) /\ et) -> ch)
Theorem	simpl31 984	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ ta /\ (ph /\ ps /\ ch)) /\ et) -> ph)
Theorem	simpl32 985	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ ta /\ (ph /\ ps /\ ch)) /\ et) -> ps)
Theorem	simpl33 986	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ ta /\ (ph /\ ps /\ ch)) /\ et) -> ch)
Theorem	simpr11 987	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((et /\ ((ph /\ ps /\ ch) /\ th /\ ta)) -> ph)
Theorem	simpr12 988	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((et /\ ((ph /\ ps /\ ch) /\ th /\ ta)) -> ps)
Theorem	simpr13 989	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((et /\ ((ph /\ ps /\ ch) /\ th /\ ta)) -> ch)
Theorem	simpr21 990	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((et /\ (th /\ (ph /\ ps /\ ch) /\ ta)) -> ph)
Theorem	simpr22 991	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((et /\ (th /\ (ph /\ ps /\ ch) /\ ta)) -> ps)
Theorem	simpr23 992	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((et /\ (th /\ (ph /\ ps /\ ch) /\ ta)) -> ch)
Theorem	simpr31 993	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((et /\ (th /\ ta /\ (ph /\ ps /\ ch))) -> ph)
Theorem	simpr32 994	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((et /\ (th /\ ta /\ (ph /\ ps /\ ch))) -> ps)
Theorem	simpr33 995	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((et /\ (th /\ ta /\ (ph /\ ps /\ ch))) -> ch)
Theorem	simp1l1 996	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th) /\ ta /\ et) -> ph)
Theorem	simp1l2 997	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th) /\ ta /\ et) -> ps)
Theorem	simp1l3 998	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th) /\ ta /\ et) -> ch)
Theorem	simp1r1 999	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch)) /\ ta /\ et) -> ph)
Theorem	simp1r2 1000	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch)) /\ ta /\ et) -> ps)