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