P. 4 of Theorem List - bfol.mm Proof Explorer

Theorem List for bfol.mm Proof Explorer - 301-400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bisym-P3.33b.CL.SYM 301	Closed Symmetric Form of bisym-P3.33b 298. †
⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))
Theorem	bitrns-P3.33c 302	Equivalence Property: '↔' Transitivity. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝛾 → (𝜑 ↔ 𝜒))
Theorem	bitrns-P3.33c.RC 303	Inference Form of bitrns-P3.33c 302. †
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜑 ↔ 𝜒)
Theorem	bitrns-P3.33c.CL 304	Closed Form of bitrns-P3.33c 302.
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜓 ↔ 𝜒)) → (𝜑 ↔ 𝜒))
4.4.2  Importation and Exportation Laws. These two laws can be thought of as justification theorems for treating a sequent of the form... 1.) '𝛾₁, 𝛾₂, ... , 𝛾n ⊢ 𝜑' as identical to the WFF statement... 2.) '⊢ ((... ((𝛾₁ ∧ 𝛾₂) ∧ 𝛾₃) ∧... 𝛾n ) → 𝜑). To obtain 2.) from 1.), first repeatedly apply ndimi-P3.5 170 to obtain a nested implication. To obtain a nested conjunction we then apply import-P3.34a.RC 306 repeatedly. To obtain 1.) from 2.), first apply export-P3.34b.RC 308 repeatedly to obtain a nested implication. From there, use a combination of ndasm-P3.1 166, ndimp-P3.2 167, and ndime-P3.6 171 repeatedly to build the sequent back up. The trivial case, '𝜑 ⊢ 𝜓 ⇔ ⊢ (𝜑 → 𝜓), cannot be replicated formally in metamath, but it is similarly justified using versions of ndasm-P3.1 166, ndimp-P3.2 167, ndimi-P3.5 170, and ndime-P3.6 171 with an empty context.
Theorem	import-P3.34a 305	'∧' Importation Law. †
⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	import-P3.34a.RC 306	Inference Form of import-P3.34a 305. †
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	export-P3.34b 307	'∧' Exportation Law. †
⊢ (𝛾 → ((𝜑 ∧ 𝜓) → 𝜒))    ⇒   ⊢ (𝛾 → (𝜑 → (𝜓 → 𝜒)))
Theorem	export-P3.34b.RC 308	Inference Form of export-P3.34b 307. †
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
4.4.2.1  Examples.
Theorem	example-E3.1a 309	Convert Sequent to Nested Implication. †
⊢ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄ ∧ 𝜑₅) → 𝜓)    ⇒   ⊢ (𝜑₁ → (𝜑₂ → (𝜑₃ → (𝜑₄ → (𝜑₅ → 𝜓)))))
Theorem	example-E3.1b 310	Convert Nested Implication to Nested Conjunction. †
⊢ (𝜑₁ → (𝜑₂ → (𝜑₃ → (𝜑₄ → (𝜑₅ → 𝜓)))))    ⇒   ⊢ (((((𝜑₁ ∧ 𝜑₂) ∧ 𝜑₃) ∧ 𝜑₄) ∧ 𝜑₅) → 𝜓)
Theorem	example-E3.2a 311	Convert Nested Conjunction to Nested Implication. †
⊢ (((((𝜑₁ ∧ 𝜑₂) ∧ 𝜑₃) ∧ 𝜑₄) ∧ 𝜑₅) → 𝜓)    ⇒   ⊢ (𝜑₁ → (𝜑₂ → (𝜑₃ → (𝜑₄ → (𝜑₅ → 𝜓)))))
Theorem	example-E3.2b 312	Convert Nested Implication to Sequent. †
⊢ (𝜑₁ → (𝜑₂ → (𝜑₃ → (𝜑₄ → (𝜑₅ → 𝜓)))))    ⇒   ⊢ ((𝜑₁ ∧ 𝜑₂ ∧ 𝜑₃ ∧ 𝜑₄ ∧ 𝜑₅) → 𝜓)
4.4.3  Commutative and Associative Properties.
Theorem	andcomm-P3.35-L1 313	Lemma for andcomm-P3.35 314. † [Auxiliary lemma - not displayed.]
Theorem	andcomm-P3.35 314	'∧' Commutativity. †
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
Theorem	andassoc-P3.36-L1 315	Lemma for andassoc-P3.36 317. † [Auxiliary lemma - not displayed.]
Theorem	andassoc-P3.36-L2 316	Lemma for andassoc-P3.36 317. † [Auxiliary lemma - not displayed.]
Theorem	andassoc-P3.36 317	'∧' Associativity. †
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
Theorem	orcomm-P3.37-L1 318	Lemma for orcomm-P3.37 319. † [Auxiliary lemma - not displayed.]
Theorem	orcomm-P3.37 319	'∨' Commutativity. †
⊢ ((𝜑 ∨ 𝜓) ↔ (𝜓 ∨ 𝜑))
Theorem	orassoc-P3.38-L1 320	Lemma for orassoc-P3.38 322. † [Auxiliary lemma - not displayed.]
Theorem	orassoc-P3.38-L2 321	Lemma for orassoc-P3.38 322. † [Auxiliary lemma - not displayed.]
Theorem	orassoc-P3.38 322	'∨' Associativity. †
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
4.4.4  Substitution Laws. These laws can be chained together to produce a countably infinite set of rules of the form... ((𝜑 ↔ 𝜓) → (𝜗 ↔ 𝜗(𝜓/𝜑)), where '𝜗' involves some combination of connectives '¬', '→', '∧', '∨', and '↔' and and contains the sub-formula '𝜑'. The notation '𝜗(𝜓/𝜑)' indicates the formula '𝜗' with one or more instances of the sub-formula '𝜑' replaced with '𝜓'. This idea will be expanded to formulas with quantifiers after developing the rules of predicate calculus. In this section we give proofs that do not use the Chapter 2 definitions of '↔', '∧', and '∨'. Those definitions, involving negation, are not valid in the intuitionist framework.
Theorem	subneg-P3.39 323	Substitution Law for '¬'. † Note that the proof of this theorem uses trnsp-P3.31c 285, which does not rely on the Law of Excluded Middle. This means this law is deducible with intuitionist logic.
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (¬ 𝜑 ↔ ¬ 𝜓))
Theorem	subneg-P3.39.RC 324	Inference Form of subneg-P3.39 323. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
Theorem	subiml-P3.40a 325	Left Substitution Law for '→'. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
Theorem	subiml-P3.40a.RC 326	Inference Form of subiml-P3.40a 325. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))
Theorem	subimr-P3.40b 327	Right Substitution Theorem for '→'. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))
Theorem	subimr-P3.40b.RC 328	Inference Form of subimr-P3.40b 327. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))
Theorem	subimd-P3.40c 329	Dual Substitution Law for '→'. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    ⇒   ⊢ (𝛾 → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜗)))
Theorem	subimd-P3.40c.RC 330	Inference Form of subimd-P3.40c 329. †
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜗)    ⇒   ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜗))
Theorem	subbil-P3.41a-L1 331	Lemma for subbil-P3.41a 332. † [Auxiliary lemma - not displayed.]
Theorem	subbil-P3.41a 332	Left Substitution Law for '↔'. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)))
Theorem	subbil-P3.41a.RC 333	Inference Form of subbil-P3.41a 332. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))
Theorem	subbir-P3.41b 334	Right Substitution Law for '↔'. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)))
Theorem	subbir-P3.41b.RC 335	Inference Form of subbir-P3.41b 334. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))
Theorem	subbid-P3.41c 336	Dual Substitution Law for '↔'. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    ⇒   ⊢ (𝛾 → ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜗)))
Theorem	subbid-P3.41c.RC 337	Inference Form of subbid-P3.41c 336. †
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜗)    ⇒   ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜗))
Theorem	subandl-P3.42a-L1 338	Lemma for subandl-P3.42a 339. † [Auxiliary lemma - not displayed.]
Theorem	subandl-P3.42a 339	Left Substitution Law for '∧'. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)))
Theorem	subandl-P3.42a.RC 340	Inference Form of subandl-P3.42a 339. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))
Theorem	subandr-P3.42b 341	Right Substitution Law for '∧'. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓)))
Theorem	subandr-P3.42b.RC 342	Inference Form of subandr-P3.42b 341. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))
Theorem	subandd-P3.42c 343	Dual Substitution Law for '∧'. †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    ⇒   ⊢ (𝛾 → ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜗)))
Theorem	subandd-P3.42c.RC 344	Inference Form of subandd-P3.42c 343. †
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜗)    ⇒   ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜗))
Theorem	suborl-P3.43a-L1 345	Lemma for suborl-P3.43a 346. † [Auxiliary lemma - not displayed.]
Theorem	suborl-P3.43a 346	Left Substitution Theorem for '∨' . †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)))
Theorem	suborl-P3.43a.RC 347	Inference Form of suborl-P3.43a 346. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))
Theorem	suborr-P3.43b 348	Right Substitution Law for '∨' . †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)))
Theorem	suborr-P3.43b.RC 349	Inference Form of suborr-P3.43b 348.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
Theorem	subord-P3.43c 350	Dual Substitution Theorem for '∨' . †
⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    ⇒   ⊢ (𝛾 → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜗)))
Theorem	subord-P3.43c.RC 351	Inference Form of subord-P3.43c 350. †
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜗)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜗))
4.4.5  Theorems for "True" and "False" Constants.
Theorem	true-P3.44 352	'⊤' is a theorem. †
⊢ ⊤
Theorem	false-P3.45 353	'⊥' is refutable. †
⊢ ¬ ⊥
4.4.6  Re-deriving Chapter 2 Definitions. In intuitionist logic, conjunction ('∧') and disjunction ('∨') are both a stronger notion than they are in the classical case. In intuitionist logic we have... '((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))' and '((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))', but not... '(¬ (𝜑 → ¬ 𝜓) → (𝜑 ∧ 𝜓))' or '((¬ 𝜑 → 𝜓) → (𝜑 ∨ 𝜓))'. The biconditional relationship '(𝜑 ↔ 𝜓)' is also stronger in the intuitionist case as it can be writter in terms of conjunction as... '((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))' which can be expanded to... '(((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))). In intuitionist logic, andasimint-P3.46b 357 allows the '∧' symbol within the left conjunct to be replaced with the primitive Hilbert definition. The same cannot be done with the right conjunct as we would need the "sufficient condition" (or "only if") part of the Hilbert definition, which is not intuitionally valid.
Theorem	andasim-P3.46-L1 354	Lemma for andasim-P3.46a 356 and andasimint-P3.46b 357. † [Auxiliary lemma - not displayed.]
Theorem	andasim-P3.46-L2 355	Lemma for andasim-P3.46a 356. [Auxiliary lemma - not displayed.]
Theorem	andasim-P3.46a 356	'∧' in Terms of '→'. This is the re-derived Chapter 2 definition. Only andasimint-P3.46b 357 is deducible with intuitionist logic.
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Theorem	andasimint-P3.46b 357	Necessary Condition for (i.e. "If" part of) '∧' Defined in Terms of '→' and '¬'. † Only this direction is deducible with intuitionist logic.
⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
Theorem	dfbi-P3.47 358	Alternate Definition of '↔'. † The Chapter 2 definition of '↔' comes immediately from combining this definition with the previous definition of '∧'. That definition really isn't useful enough to state though.
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
Theorem	orasim-P3.48-L1 359	Lemma for orasim-P3.48a 361 and orasimint-P3.48b 362. † [Auxiliary lemma - not displayed.]
Theorem	orasim-P3.48-L2 360	Lemma for orasim-P3.48a 361. [Auxiliary lemma - not displayed.]
Theorem	orasim-P3.48a 361	'∨' in Terms of '→'. This is the re-derived Chapter 2 definition. Only orasimint-P3.48b 362 is deducible with intuitionist logic.
⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
Theorem	orasimint-P3.48b 362	Necessary Condition for (i.e. "If" part of) '∨' Defined in Terms of '→' and '¬'. † Only this direction is deducible with intuitionist logic.
⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
Theorem	dffalse-P3.49-L1 363	Lemma for dffalse-P3.49 365. † [Auxiliary lemma - not displayed.]
Theorem	dffalse-P3.49-L2 364	Lemma for dffalse-P3.49 365. † [Auxiliary lemma - not displayed.]
Theorem	dffalse-P3.49 365	Re-derived Chapter 2 '⊥' definition. †
⊢ (⊥ ↔ ¬ ⊤)
PART 5  Chapter 4: Propositional Calculus (continued)
5.1  More Useful Rules.
5.1.1  Law of Non-contradiction.
Theorem	ncontra-P4.1 366	Law of Non-contradiction. †
⊢ ¬ (𝜑 ∧ ¬ 𝜑)
5.1.2  Dual Forms of Introduction and Elimination Rules.
Theorem	norel-P4.2a 367	Negated Left '∨' Elimination. †
⊢ (𝛾 → ¬ (𝜑 ∨ 𝜓))    ⇒   ⊢ (𝛾 → ¬ 𝜓)
Theorem	norel-P4.2a.RC 368	Inference Form of norel-P4.2a 367. †
⊢ ¬ (𝜑 ∨ 𝜓)    ⇒   ⊢ ¬ 𝜓
Theorem	norel-P4.2a.CL 369	Closed Form of norel-P4.2a 367. †
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜓)
Theorem	norer-P4.2b 370	Negated Right '∨' Elimination. †
⊢ (𝛾 → ¬ (𝜑 ∨ 𝜓))    ⇒   ⊢ (𝛾 → ¬ 𝜑)
Theorem	norer-P4.2b.RC 371	Inference Form of norer-P4.2b 370. †
⊢ ¬ (𝜑 ∨ 𝜓)    ⇒   ⊢ ¬ 𝜑
Theorem	norer-P4.2b.CL 372	Closed Form of norer-P4.2b 370. †
⊢ (¬ (𝜑 ∨ 𝜓) → ¬ 𝜑)
Theorem	nandil-P4.3a 373	Negated Left '∧' Introduction. †
⊢ (𝛾 → ¬ 𝜑)    ⇒   ⊢ (𝛾 → ¬ (𝜓 ∧ 𝜑))
Theorem	nandil-P4.3a.RC 374	Inference Form of nandil-P4.3a 373. †
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜓 ∧ 𝜑)
Theorem	nandir-P4.3b 375	Negated Right '∧' Introduction. †
⊢ (𝛾 → ¬ 𝜑)    ⇒   ⊢ (𝛾 → ¬ (𝜑 ∧ 𝜓))
Theorem	nandir-P4.3b.RC 376	Inference Form of nandir-P4.3b 375. †
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜑 ∧ 𝜓)
5.1.3  Other Forms of the Principle Of Explosion.
Theorem	impoe-P4.4a 377	Variation of Principle of Explosion Using Implication. †
⊢ (𝛾 → ¬ 𝜑)    ⇒   ⊢ (𝛾 → (𝜑 → 𝜓))
Theorem	impoe-P4.4a.RC 378	Inference Form of impoe-P4.4a 377. †
⊢ ¬ 𝜑    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	impoe-P4.4a.CL 379	Closed Form of impoe-P4.4a 377. †
⊢ (¬ 𝜑 → (𝜑 → 𝜓))
Theorem	nimpoe-P4.4b 380	Variation of Principle of Explosion Using Implication (negated form). †
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → (¬ 𝜑 → 𝜓))
Theorem	nimpoe-P4.4b.RC 381	Inference Form of nimpoe-P4.4b 380. †
⊢ 𝜑    ⇒   ⊢ (¬ 𝜑 → 𝜓)
Theorem	nimpoe-P4.4b.CL 382	Closed Form of nimpoe-P4.4b 380. †
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
Theorem	falseimpoe-P4.4c 383	Principle of Explosion Utilising '⊥'. †
⊢ (𝛾 → ⊥)    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	falseimpoe-P4.4c.RC 384	Inference Form of falseimpoe-P4.4c 383. † In an inconsistent system, every wff is a theorem.
⊢ ⊥    ⇒   ⊢ 𝜑
5.1.4  Process of Elimination.
Theorem	profeliml-P4.5a 385	Process of Elimination (left). †
⊢ (𝛾 → (𝜑 ∨ 𝜓))    &   ⊢ (𝛾 → ¬ 𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	profeliml-P4.5a.RC 386	Inference Form of profeliml-P4.5a 385. †
⊢ (𝜑 ∨ 𝜓)    &   ⊢ ¬ 𝜑    ⇒   ⊢ 𝜓
Theorem	profelimr-P4.5b 387	Process of Elimination (right). †
⊢ (𝛾 → (𝜑 ∨ 𝜓))    &   ⊢ (𝛾 → ¬ 𝜓)    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	profelimr-P4.5b.RC 388	Inference Form of profelimr-P4.5b 387. †
⊢ (𝜑 ∨ 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ 𝜑
Theorem	nprofeliml-P4.6a 389	Negated Process of Elimination (left). †
⊢ (𝛾 → ¬ (𝜑 ∧ 𝜓))    &   ⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ¬ 𝜓)
Theorem	nprofeliml-P4.6a.RC 390	Inference Form of nprofeliml-P4.6a 389. †
⊢ ¬ (𝜑 ∧ 𝜓)    &   ⊢ 𝜑    ⇒   ⊢ ¬ 𝜓
Theorem	nprofelimr-P4.6b 391	Negated Process of Elimination (right). †
⊢ (𝛾 → ¬ (𝜑 ∧ 𝜓))    &   ⊢ (𝛾 → 𝜓)    ⇒   ⊢ (𝛾 → ¬ 𝜑)
Theorem	nprofelimr-P4.6b.RC 392	Inference Form of nprofelimr-P4.6b 391. †
⊢ ¬ (𝜑 ∧ 𝜓)    &   ⊢ 𝜓    ⇒   ⊢ ¬ 𝜑
Theorem	falseprofeliml-P4.7a 393	Process of Elimination Utilising '⊥' (left). †
⊢ (𝛾 → (𝜑 ∨ 𝜓))    &   ⊢ (𝛾 → (𝜑 → ⊥))    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	falseprofeliml-P4.7a.RC 394	Inference Form of falseprofeliml-P4.7a 393. †
⊢ (𝜑 ∨ 𝜓)    &   ⊢ (𝜑 → ⊥)    ⇒   ⊢ 𝜓
Theorem	falseprofelimr-P4.7b 395	Process of Elimination Utilizing '⊥' (right). †
⊢ (𝛾 → (𝜑 ∨ 𝜓))    &   ⊢ (𝛾 → (𝜓 → ⊥))    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	falseprofelimr-P4.7b.RC 396	Inference Form of falseprofelimr-P4.7b 395. †
⊢ (𝜑 ∨ 𝜓)    &   ⊢ (𝜓 → ⊥)    ⇒   ⊢ 𝜑
5.1.5  Joining Implications.
Theorem	joinimandinc-P4.8a 397	Join Two Implications Through Conjunction (Inclusive). †
⊢ (𝛾 → ((𝜑 → 𝜓) ∧ (𝜒 → 𝜗)))    ⇒   ⊢ (𝛾 → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜗)))
Theorem	joinimandinc-P4.8a.RC 398	Inference Form of joinimandinc-P4.8a 397. †
⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜗))    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜗))
Theorem	joinimandinc-P4.8a.CL 399	Closed Form of joinimandinc-P4.8a 397. †
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜗)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜗)))
Theorem	joinimandres-P4.8b 400	Join Two Implications Through Conjunction (Restrictive). †
⊢ (𝛾 → ((𝜑 → 𝜓) ∧ (𝜒 → 𝜗)))    ⇒   ⊢ (𝛾 → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜗)))