P. 340 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33901-34000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	exmid2 33901	An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.)
|- ( ( ps /\ ph ) -> ch )   &    |- ( ( -. ps /\ et ) -> ch )   =>    |- ( ( ph /\ et ) -> ch )
Theorem	selconj 33902	An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ( et /\ ph ) <-> ( ps /\ ( et /\ ch ) ) )
Theorem	truconj 33903	Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.)
|- ( ph <-> ( T. /\ ph ) )
Theorem	orel 33904	An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- ( ( ps /\ et ) -> th )   &    |- ( ( ch /\ rh ) -> th )   &    |- ( ph -> ( ps \/ ch ) )   =>    |- ( ( ph /\ ( et /\ rh ) ) -> th )
Theorem	negel 33905	An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- ( ps -> ch )   &    |- ( ph -> -. ch )   =>    |- ( ( ph /\ ps ) -> F. )
Theorem	botel 33906	An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- ( ph -> F. )   =>    |- ( ph -> ps )
Theorem	tradd 33907	Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- ( ph <-> ps )   =>    |- ( ph <-> ( T. /\ ps ) )
Theorem	sbtru 33908	Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. T. <-> T. )
Theorem	sbfal 33909	Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. F. <-> F. )
Theorem	sbcani 33910	Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- ( [. A / x ]. ph <-> ch )   &    |- ( [. A / x ]. ps <-> et )   =>    |- ( [. A / x ]. ( ph /\ ps ) <-> ( ch /\ et ) )
Theorem	sbcori 33911	Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- ( [. A / x ]. ph <-> ch )   &    |- ( [. A / x ]. ps <-> et )   =>    |- ( [. A / x ]. ( ph \/ ps ) <-> ( ch \/ et ) )
Theorem	sbcimi 33912	Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   &    |- ( [. A / x ]. ph <-> ch )   &    |- ( [. A / x ]. ps <-> et )   =>    |- ( [. A / x ]. ( ph -> ps ) <-> ( ch -> et ) )
Theorem	sbceqi 33913	Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   &    |- [_ A / x ]_ B = D   &    |- [_ A / x ]_ C = E   =>    |- ( [. A / x ]. B = C <-> D = E )
Theorem	sbcni 33914	Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   &    |- ( [. A / x ]. ph <-> ps )   =>    |- ( [. A / x ]. -. ph <-> -. ps )
Theorem	sbali 33915	Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. A. x ph <-> A. x ph )
Theorem	sbexi 33916	Discard class substitution in an existential quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. E. x ph <-> E. x ph )
Theorem	sbcalf 33917*	Move universal quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
|- F/_ y A   =>    |- ( [. A / x ]. A. y ph <-> A. y [. A / x ]. ph )
Theorem	sbcexf 33918*	Move existential quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.)
|- F/_ y A   =>    |- ( [. A / x ]. E. y ph <-> E. y [. A / x ]. ph )
Theorem	sbcalfi 33919*	Move universal quantifier in and out of class substitution, with an explicit non-free variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- F/_ y A   &    |- ( [. A / x ]. ph <-> ps )   =>    |- ( [. A / x ]. A. y ph <-> A. y ps )
Theorem	sbcexfi 33920*	Move existential quantifier in and out of class substitution, with an explicit non-free variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- F/_ y A   &    |- ( [. A / x ]. ph <-> ps )   =>    |- ( [. A / x ]. E. y ph <-> E. y ps )
Theorem	csbvargi 33921	The proper substitution of a class for a variable in that variable results in the class (if the class exists), in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- A e. _V   =>    |- [_ A / x ]_ x = A
Theorem	csbconstgi 33922*	The proper substitution of a class for a variable in another variable does not modify it, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- A e. _V   =>    |- [_ A / x ]_ y = y
Theorem	spsbcdi 33923	A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- A e. _V   &    |- ( ph -> A. x ch )   &    |- ( [. A / x ]. ch <-> ps )   =>    |- ( ph -> ps )
Theorem	alrimii 33924*	A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- F/ y ph   &    |- ( ph -> ps )   &    |- ( [. y / x ]. ch <-> ps )   &    |- F/ y ch   =>    |- ( ph -> A. x ch )
Theorem	spesbcdi 33925	A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- ( ph -> ps )   &    |- ( [. A / x ]. ch <-> ps )   =>    |- ( ph -> E. x ch )
Theorem	exlimddvf 33926	A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.)
|- ( ph -> E. x th )   &    |- F/ x ps   &    |- ( ( th /\ ps ) -> ch )   &    |- F/ x ch   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	exlimddvfi 33927	A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- ( ph -> E. x th )   &    |- F/ y th   &    |- F/ y ps   &    |- ( [. y / x ]. th <-> et )   &    |- ( ( et /\ ps ) -> ch )   &    |- F/ y ch   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	sbceq1ddi 33928	A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- ( ph -> A = B )   &    |- ( ps -> th )   &    |- ( [. A / x ]. ch <-> th )   &    |- ( [. B / x ]. ch <-> et )   =>    |- ( ( ph /\ ps ) -> et )
Theorem	sbccom2lem 33929*	Lemma for sbccom2 33930. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
Theorem	sbccom2 33930*	Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- A e. _V   =>    |- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
Theorem	sbccom2f 33931*	Commutative law for double class substitution, with non free variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.)
|- A e. _V   &    |- F/_ y A   =>    |- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
Theorem	sbccom2fi 33932*	Commutative law for double class substitution, with non free variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
|- A e. _V   &    |- F/_ y A   &    |- [_ A / x ]_ B = C   &    |- ( [. A / x ]. ph <-> ps )   =>    |- ( [. A / x ]. [. B / y ]. ph <-> [. C / y ]. ps )
Theorem	sbcgfi 33933	Substitution for a variable not free in a wff does not affect it, in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.)
|- A e. _V   &    |- F/ x ph   =>    |- ( [. A / x ]. ph <-> ph )
Theorem	csbcom2fi 33934*	Commutative law for double class substitution in a class, with non free variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
|- A e. _V   &    |- F/_ y A   &    |- [_ A / x ]_ B = C   &    |- [_ A / x ]_ D = E   =>    |- [_ A / x ]_ [_ B / y ]_ D = [_ C / y ]_ E
Theorem	csbgfi 33935	Substitution for a variable not free in a class does not affect it, in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.)
|- A e. _V   &    |- F/_ x B   =>    |- [_ A / x ]_ B = B
20.20.2  Tseitin axioms A collection of Tseitin axioms used to convert a wff to Conjunctive Normal Form.
Theorem	fald 33936	Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> -. F. )
Theorem	tsim1 33937	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ ps ) \/ -. ( ph -> ps ) ) )
Theorem	tsim2 33938	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ph \/ ( ph -> ps ) ) )
Theorem	tsim3 33939	A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( -. ps \/ ( ph -> ps ) ) )
Theorem	tsbi1 33940	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ -. ps ) \/ ( ph <-> ps ) ) )
Theorem	tsbi2 33941	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( ph \/ ps ) \/ ( ph <-> ps ) ) )
Theorem	tsbi3 33942	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( ph \/ -. ps ) \/ -. ( ph <-> ps ) ) )
Theorem	tsbi4 33943	A Tseitin axiom for logical biimplication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ ps ) \/ -. ( ph <-> ps ) ) )
Theorem	tsxo1 33944	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ -. ps ) \/ -. ( ph \/_ ps ) ) )
Theorem	tsxo2 33945	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( ph \/ ps ) \/ -. ( ph \/_ ps ) ) )
Theorem	tsxo3 33946	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( ph \/ -. ps ) \/ ( ph \/_ ps ) ) )
Theorem	tsxo4 33947	A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ ps ) \/ ( ph \/_ ps ) ) )
Theorem	tsan1 33948	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ -. ps ) \/ ( ph /\ ps ) ) )
Theorem	tsan2 33949	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ph \/ -. ( ph /\ ps ) ) )
Theorem	tsan3 33950	A Tseitin axiom for logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ps \/ -. ( ph /\ ps ) ) )
Theorem	tsna1 33951	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ( -. ph \/ -. ps ) \/ -. ( ph -/\ ps ) ) )
Theorem	tsna2 33952	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ph \/ ( ph -/\ ps ) ) )
Theorem	tsna3 33953	A Tseitin axiom for logical incompatibility, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.)
|- ( th -> ( ps \/ ( ph -/\ ps ) ) )
Theorem	tsor1 33954	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
|- ( th -> ( ( ph \/ ps ) \/ -. ( ph \/ ps ) ) )
Theorem	tsor2 33955	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
|- ( th -> ( -. ph \/ ( ph \/ ps ) ) )
Theorem	tsor3 33956	A Tseitin axiom for logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
|- ( th -> ( -. ps \/ ( ph \/ ps ) ) )
Theorem	ts3an1 33957	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
|- ( th -> ( ( -. ( ph /\ ps ) \/ -. ch ) \/ ( ph /\ ps /\ ch ) ) )
Theorem	ts3an2 33958	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
|- ( th -> ( ( ph /\ ps ) \/ -. ( ph /\ ps /\ ch ) ) )
Theorem	ts3an3 33959	A Tseitin axiom for triple logical conjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
|- ( th -> ( ch \/ -. ( ph /\ ps /\ ch ) ) )
Theorem	ts3or1 33960	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
|- ( th -> ( ( ( ph \/ ps ) \/ ch ) \/ -. ( ph \/ ps \/ ch ) ) )
Theorem	ts3or2 33961	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
|- ( th -> ( -. ( ph \/ ps ) \/ ( ph \/ ps \/ ch ) ) )
Theorem	ts3or3 33962	A Tseitin axiom for triple logical disjunction, in deduction form. (Contributed by Giovanni Mascellani, 25-Mar-2018.)
|- ( th -> ( -. ch \/ ( ph \/ ps \/ ch ) ) )
20.20.3  Equality deductions A collection of theorems for commuting equalities (or biimplications) with other constructs.
Theorem	iuneq2f 33963	Equality deduction for indexed union. (Contributed by Giovanni Mascellani, 9-Apr-2018.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B -> U_ x e. A C = U_ x e. B C )
Theorem	abeq12 33964	Equality deduction for class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- ( A. x ( ph <-> ps ) -> { x | ph } = { x | ps } )
Theorem	rabeq12f 33965	Equality deduction for restricted class abstraction. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( ( A = B /\ A. x e. A ( ph <-> ps ) ) -> { x e. A | ph } = { x e. B | ps } )
Theorem	csbeq12 33966	Equality deduction for substitution in class. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- ( ( A = B /\ A. x C = D ) -> [_ A / x ]_ C = [_ B / x ]_ D )
Theorem	nfbii2 33967	Equality deduction for not-freeness. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- ( A. x ( ph <-> ps ) -> ( F/ x ph <-> F/ x ps ) )
Theorem	sbeqi 33968	Equality deduction for substitution. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- ( ( x = y /\ A. z ( ph <-> ps ) ) -> ( [ x / z ] ph <-> [ y / z ] ps ) )
Theorem	ralbi12f 33969	Equality deduction for restricted universal quantification. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( ( A = B /\ A. x e. A ( ph <-> ps ) ) -> ( A. x e. A ph <-> A. x e. B ps ) )
Theorem	oprabbi 33970	Equality deduction for class abstraction of nested ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- ( A. x A. y A. z ( ph <-> ps ) -> { <. <. x , y >. , z >. | ph } = { <. <. x , y >. , z >. | ps } )
Theorem	mpt2bi123f 33971*	Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- F/_ x A   &    |- F/_ x B   &    |- F/_ y A   &    |- F/_ y B   &    |- F/_ y C   &    |- F/_ y D   &    |- F/_ x C   &    |- F/_ x D   =>    |- ( ( ( A = B /\ C = D ) /\ A. x e. A A. y e. C E = F ) -> ( x e. A , y e. C |-> E ) = ( x e. B , y e. D |-> F ) )
Theorem	iuneq12f 33972	Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( ( A = B /\ A. x e. A C = D ) -> U_ x e. A C = U_ x e. B D )
Theorem	iineq12f 33973	Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( ( A = B /\ A. x e. A C = D ) -> |^|_ x e. A C = |^|_ x e. B D )
Theorem	opabbi 33974	Equality deduction for class abstraction of ordered pairs. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- ( A. x A. y ( ph <-> ps ) -> { <. x , y >. | ph } = { <. x , y >. | ps } )
Theorem	mptbi12f 33975	Equality deduction for maps-to notations. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( ( A = B /\ A. x e. A D = E ) -> ( x e. A |-> D ) = ( x e. B |-> E ) )
20.20.4  Miscellanea Work in progress or things that do not belong anywhere else.
Theorem	scottexf 33976*	A version of scottex 8748 with non-free variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
|- F/_ y A   &    |- F/_ x A   =>    |- { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V
Theorem	scott0f 33977*	A version of scott0 8749 with non-free variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
|- F/_ y A   &    |- F/_ x A   =>    |- ( A = (/) <-> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = (/) )
Theorem	scottn0f 33978*	A version of scott0f 33977 with inequalities instead of equalities. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
|- F/_ y A   &    |- F/_ x A   =>    |- ( A =/= (/) <-> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } =/= (/) )
Theorem	ac6s3f 33979*	Generalization of the Axiom of Choice to classes, with bound-variable hypothesis. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
|- F/ y ps   &    |- A e. _V   &    |- ( y = ( f ` x ) -> ( ph <-> ps ) )   =>    |- ( A. x e. A E. y ph -> E. f A. x e. A ps )
Theorem	ac6s6 33980*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
|- F/ y ps   &    |- A e. _V   &    |- ( y = ( f ` x ) -> ( ph <-> ps ) )   =>    |- E. f A. x e. A ( E. y ph -> ps )
Theorem	ac6s6f 33981*	Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 20-Aug-2018.)
|- A e. _V   &    |- F/ y ps   &    |- ( y = ( f ` x ) -> ( ph <-> ps ) )   &    |- F/_ x A   =>    |- E. f A. x e. A ( E. y ph -> ps )
20.21  Mathbox for Peter Mazsa
20.21.1  Notations
Syntax	cxrn 33982	Extend the definition of a class to include the range Cartesian product class.
class ( A |X. B )
20.21.2  Preparatory theorems
Theorem	elv 33983	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. Inference forms (with A e. _V hypotheses) of the general theorems (proving A e. V ->) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.)
|- ( x e. _V -> ph )   =>    |- ph
Theorem	el2v 33984	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. Inference forms (with A e. _V and B e. _V hypotheses) of the general theorems (proving ( A e. V /\ B e. W ) ->) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.)
|- ( ( x e. _V /\ y e. _V ) -> ph )   =>    |- ph
Theorem	el2v1 33985	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.)
|- ( ( x e. _V /\ ph ) -> ps )   =>    |- ( ph -> ps )
Theorem	el2v2 33986	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 23-Oct-2018.)
|- ( ( ph /\ y e. _V ) -> ps )   =>    |- ( ph -> ps )
Theorem	el3v 33987	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. Inference forms (with A e. _V, B e. _V and C e. _V hypotheses) of the general theorems (proving ( A e. V /\ B e. W /\ C e. X ) ->) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.)
|- ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ph )   =>    |- ph
Theorem	el3v1 33988	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
|- ( ( x e. _V /\ ps /\ ch ) -> th )   =>    |- ( ( ps /\ ch ) -> th )
Theorem	el3v2 33989	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
|- ( ( ph /\ y e. _V /\ ch ) -> th )   =>    |- ( ( ph /\ ch ) -> th )
Theorem	el3v3 33990	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 16-Oct-2020.)
|- ( ( ph /\ ps /\ z e. _V ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	el3v12 33991	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
|- ( ( x e. _V /\ y e. _V /\ ch ) -> th )   =>    |- ( ch -> th )
Theorem	el3v13 33992	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
|- ( ( x e. _V /\ ps /\ z e. _V ) -> th )   =>    |- ( ps -> th )
Theorem	el3v23 33993	New way (elv 33983, el2v 33984 theorems and el3v 33987 theorems) to shorten some proofs. (Contributed by Peter Mazsa, 11-Jul-2021.)
|- ( ( ph /\ y e. _V /\ z e. _V ) -> th )   =>    |- ( ph -> th )
Theorem	biancom 33994	Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018.)
|- ( ph <-> ( ch /\ ps ) )   =>    |- ( ph <-> ( ps /\ ch ) )
Theorem	biancomd 33995	Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.)
|- ( ph -> ( ps <-> ( th /\ ch ) ) )   =>    |- ( ph -> ( ps <-> ( ch /\ th ) ) )
Theorem	anbi1ci 33996	Introduce a left and the same right conjunct to the sides of a logical equivalence. (Contributed by Peter Mazsa, 7-Mar-2020.)
|- ( ph <-> ps )   =>    |- ( ( ch /\ ph ) <-> ( ps /\ ch ) )
Theorem	anbi1cd 33997	Introduce a left and the same right conjunct to the sides of a logical equivalence, deduction form. (Contributed by Peter Mazsa, 22-May-2021.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th /\ ps ) <-> ( ch /\ th ) ) )
Theorem	an2anr 33998	Double commutation in conjunction. (Contributed by Peter Mazsa, 27-Jun-2019.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ps /\ ph ) /\ ( th /\ ch ) ) )
Theorem	anan 33999	Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ ( ( ph /\ th ) /\ ta ) ) <-> ( ( ps /\ th ) /\ ( ph /\ ( ch /\ ta ) ) ) )
Theorem	triantru3 34000	A wff is equivalent to its conjunctions with truths. (Contributed by Peter Mazsa, 30-Nov-2018.)
|- ph   &    |- ps   =>    |- ( ch <-> ( ph /\ ps /\ ch ) )