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

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

Type	Label	Description
Statement
Theorem	truthtblfandt-P4.37c 501	( F ∧ T ) ⇔ F. †
⊢ ((⊥ ∧ ⊤) ↔ ⊥)
Theorem	truthtblfandf-P4.37d 502	( F ∧ F ) ⇔ F. †
⊢ ((⊥ ∧ ⊥) ↔ ⊥)
5.2.9.4  Disjunction.
Theorem	truthtbltort-P4.38a 503	( T ∨ T ) ⇔ T. †
⊢ ((⊤ ∨ ⊤) ↔ ⊤)
Theorem	truthtbltorf-P4.38b 504	( T ∨ F ) ⇔ T. †
⊢ ((⊤ ∨ ⊥) ↔ ⊤)
Theorem	truthtblfort-P4.38c 505	( F ∨ T ) ⇔ T. †
⊢ ((⊥ ∨ ⊤) ↔ ⊤)
Theorem	truthtblforf-P4.38d 506	( F ∨ F ) ⇔ F. †
⊢ ((⊥ ∨ ⊥) ↔ ⊥)
5.2.9.5  Equivalence.
Theorem	truthtbltbit-P4.39a 507	( T ↔ T ) ⇔ T. †
⊢ ((⊤ ↔ ⊤) ↔ ⊤)
Theorem	truthtbltbif-P4.39b 508	( T ↔ F ) ⇔ F. †
⊢ ((⊤ ↔ ⊥) ↔ ⊥)
Theorem	truthtblfbit-P4.39c 509	( F ↔ T ) ⇔ F. †
⊢ ((⊥ ↔ ⊤) ↔ ⊥)
Theorem	truthtblfbif-P4.39d 510	( F ↔ F ) ⇔ T. †
⊢ ((⊥ ↔ ⊥) ↔ ⊤)
5.3  Peirce's Law.
5.3.1  Classical Proof.
Theorem	peirce-P4.40 511	Peirce's Law. Cannot be proven without the Law of Excluded Middle.
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
5.3.2  Equivalence of Peirce's Law and Law of Excluded Middle.
Theorem	exclmid2peirce-P4.41a 512	Peirce's Law from Law of Excluded Middle. † The use of ndexclmid-P3.16 181 is simply replaced with a hypothesis. All the other rules used are valid in intuitionist logic.
⊢ (𝜑 ∨ ¬ 𝜑)    ⇒   ⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	peirce2exclmid-P4.41b 513	Law of Excluded Middle from Peirce's Law. † The hypothesis is a special case of Peirce's Law.
⊢ ((((𝜑 ∨ ¬ 𝜑) → ⊥) → (𝜑 ∨ ¬ 𝜑)) → (𝜑 ∨ ¬ 𝜑))    ⇒   ⊢ (𝜑 ∨ ¬ 𝜑)
5.4  Appendix: Miscellaneous Utility Rules.
5.4.1  Reductio ad Absurdum. This scheme relies on the Law of Excluded Middle.
5.4.1.1  Rule.
Theorem	raa-P4 514	Reductio ad Absurdum. This rule combines ndnegi-P3.3 168 with double negative elimination, and is thus dependent on the Law of Excluded Middle.
⊢ ((𝛾 ∧ ¬ 𝜑) → 𝜓)    &   ⊢ ((𝛾 ∧ ¬ 𝜑) → ¬ 𝜓)    ⇒   ⊢ (𝛾 → 𝜑)
5.4.1.2  Scheme. These derived rules may be used in place of raa-P4 514.
Theorem	rcp-RAA1 515	Reductio ad Absurdum.
⊢ (¬ 𝛾₁ → 𝜑)    &   ⊢ (¬ 𝛾₁ → ¬ 𝜑)    ⇒   ⊢ 𝛾₁
Theorem	rcp-RAA2 516	Reductio ad Absurdum.
⊢ ((𝛾₁ ∧ ¬ 𝛾₂) → 𝜑)    &   ⊢ ((𝛾₁ ∧ ¬ 𝛾₂) → ¬ 𝜑)    ⇒   ⊢ (𝛾₁ → 𝛾₂)
Theorem	rcp-RAA3 517	Reductio ad Absurdum.
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ ¬ 𝛾₃) → 𝜑)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ ¬ 𝛾₃) → ¬ 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂) → 𝛾₃)
Theorem	rcp-RAA4 518	Reductio ad Absurdum.
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ ¬ 𝛾₄) → 𝜑)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ ¬ 𝛾₄) → ¬ 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝛾₄)
Theorem	rcp-RAA5 519	Reductio ad Absurdum.
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ ¬ 𝛾₅) → 𝜑)    &   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ ¬ 𝛾₅) → ¬ 𝜑)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝛾₅)
5.4.2  Reductio ad Absurdum Using "False" Constant.
5.4.2.1  Rule.
Theorem	falseraa-P4 520	Reductio ad Absurdum Using '⊥'. This rule combines falsenegi-P4.18 432 with double negative elimination, and is thus dependent on the Law of Excluded Middle.
⊢ ((𝛾 ∧ ¬ 𝜑) → ⊥)    ⇒   ⊢ (𝛾 → 𝜑)
5.4.2.2  Scheme. These derived rules may be used in place of falseraa-P4 520.
Theorem	rcp-FALSERAA1 521	Reductio ad Absurdum Using '⊥'.
⊢ (¬ 𝛾₁ → ⊥)    ⇒   ⊢ 𝛾₁
Theorem	rcp-FALSERAA2-P 522	Reductio ad Absurdum Using '⊥'.
⊢ ((𝛾₁ ∧ ¬ 𝛾₂) → ⊥)    ⇒   ⊢ (𝛾₁ → 𝛾₂)
Theorem	rcp-FALSERAA3 523	Reductio ad Absurdum Using '⊥'.
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ ¬ 𝛾₃) → ⊥)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂) → 𝛾₃)
Theorem	rcp-FALSERAA4 524	Reductio ad Absurdum Using '⊥'.
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ ¬ 𝛾₄) → ⊥)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → 𝛾₄)
Theorem	rcp-FALSERAA5 525	Reductio ad Absurdum Using '⊥'.
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ ¬ 𝛾₅) → ⊥)    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → 𝛾₅)
5.4.3  Convert Implication to Assumption.
5.4.3.1  Rule.
Theorem	impime-P4 526	'→' Elimination with Importation. †
⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ ((𝛾 ∧ 𝜑) → 𝜓)
5.4.3.2  Scheme. These derived rules may be used in place of impime-P4 526.
Theorem	rcp-IMPIME1 527	'→' Elimination with Importation. †
⊢ (𝛾₁ → (𝜑 → 𝜓))    ⇒   ⊢ ((𝛾₁ ∧ 𝜑) → 𝜓)
Theorem	rcp-IMPIME2 528	'→' Elimination with Importation. †
⊢ ((𝛾₁ ∧ 𝛾₂) → (𝜑 → 𝜓))    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝜑) → 𝜓)
Theorem	rcp-IMPIME3 529	'→' Elimination with Importation. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃) → (𝜑 → 𝜓))    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝜑) → 𝜓)
Theorem	rcp-IMPIME4 530	'→' Elimination with Importation. †
⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄) → (𝜑 → 𝜓))    ⇒   ⊢ ((𝛾₁ ∧ 𝛾₂ ∧ 𝛾₃ ∧ 𝛾₄ ∧ 𝜑) → 𝜓)
5.4.4  Combine Biconditional Elimination with Modus Ponens.
Theorem	bimpf-P4 531	Modus Ponens with '↔' (forward). †
⊢ (𝛾 → 𝜑)    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	bimpf-P4.RC 532	Inference Form of bimpf-P4 531. †
⊢ 𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝜓
Theorem	bimpr-P4 533	Modus Ponens with '↔' (reverse). †
⊢ (𝛾 → 𝜓)    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	bimpr-P4.RC 534	Inference Form of bimpr-P4 533. †
⊢ 𝜓    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝜑
5.4.5  Transposition Laws as Equivalence Laws.
Theorem	trnspeq-P4a 535	Transposition Equivalence Law (trnsp-P3.31a 279). †
⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑))
Theorem	trnspeq-P4b 536	Transposition Equivalence Law (trnsp-P3.31b 282).
⊢ ((¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → 𝜑))
Theorem	trnspeq-P4c 537	Transposition Equivalence Law (trnsp-P3.31c 285 and trnsp-P3.31d 288).
⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑))
5.4.6  Different Form for Substitution Laws.
Theorem	subneg2-P4 538	Alternate Form of subneg-P3.39 323. †
⊢ (𝛾 → ¬ 𝜑)    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → ¬ 𝜓)
Theorem	subneg2-P4.RC 539	Inference Form of subneg2-P4 538. †
⊢ ¬ 𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ 𝜓
Theorem	subiml2-P4 540	Alternate Form of subiml-P3.40a 325. †
⊢ (𝛾 → (𝜑 → 𝜒))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 → 𝜒))
Theorem	subiml2-P4.RC 541	Inference Form of subiml2-P4 540. †
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	subimr2-P4 542	Alternate Form of subimr-P3.40b 327. †
⊢ (𝛾 → (𝜒 → 𝜑))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜒 → 𝜓))
Theorem	subimr2-P4.RC 543	Inference Form of subimr2-P4 542. †
⊢ (𝜒 → 𝜑)    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜒 → 𝜓)
Theorem	subimd2-P4 544	Alternate Form of subimd-P3.40c 329. †
⊢ (𝛾 → (𝜑 → 𝜒))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    ⇒   ⊢ (𝛾 → (𝜓 → 𝜗))
Theorem	subimd2-P4.RC 545	Inference Form of subimd2-P4 544. †
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜗)    ⇒   ⊢ (𝜓 → 𝜗)
Theorem	subbil2-P4 546	Alternate Form of subbil-P3.41a 332. †
⊢ (𝛾 → (𝜑 ↔ 𝜒))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 ↔ 𝜒))
Theorem	subbil2-P4.RC 547	Inference Form of subbil2-P4 546. †
⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 ↔ 𝜒)
Theorem	subbir2-P4 548	Alternate Form of subbir-P3.41b 334. †
⊢ (𝛾 → (𝜒 ↔ 𝜑))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜒 ↔ 𝜓))
Theorem	subbir2-P4.RC 549	Inference Form of subbir2-P4 548. †
⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜒 ↔ 𝜓)
Theorem	subbid2-P4 550	Alternate Form of subbid-P3.41c 336. †
⊢ (𝛾 → (𝜑 ↔ 𝜒))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    ⇒   ⊢ (𝛾 → (𝜓 ↔ 𝜗))
Theorem	subbid2-P4.RC 551	Inference Form of subbid2-P4 550. †
⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜗)    ⇒   ⊢ (𝜓 ↔ 𝜗)
Theorem	subandl2-P4 552	Alternate Form of subandl-P3.42a 339. †
⊢ (𝛾 → (𝜑 ∧ 𝜒))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 ∧ 𝜒))
Theorem	subandl2-P4.RC 553	Inference Form of subandl2-P4 552. †
⊢ (𝜑 ∧ 𝜒)    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 ∧ 𝜒)
Theorem	subandr2-P4 554	Alternate Form of subandr-P3.42b 341. †
⊢ (𝛾 → (𝜒 ∧ 𝜑))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜒 ∧ 𝜓))
Theorem	subandr2-P4.RC 555	Inference Form of subandr2-P4 554. †
⊢ (𝜒 ∧ 𝜑)    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜒 ∧ 𝜓)
Theorem	subandd2-P4 556	Alternate Form of subandd-P3.42c 343. †
⊢ (𝛾 → (𝜑 ∧ 𝜒))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    ⇒   ⊢ (𝛾 → (𝜓 ∧ 𝜗))
Theorem	subandd2-P4.RC 557	Inference Form of subandd2-P4 556. †
⊢ (𝜑 ∧ 𝜒)    &   ⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜗)    ⇒   ⊢ (𝜓 ∧ 𝜗)
Theorem	suborl2-P4 558	Alternate Form of suborl-P3.43a 346. †
⊢ (𝛾 → (𝜑 ∨ 𝜒))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 ∨ 𝜒))
Theorem	suborl2-P4.RC 559	Inference Form of suborl2-P4 558. †
⊢ (𝜑 ∨ 𝜒)    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 ∨ 𝜒)
Theorem	suborr2-P4 560	Alternate Form of suborr-P3.43b 348. †
⊢ (𝛾 → (𝜒 ∨ 𝜑))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (𝜒 ∨ 𝜓))
Theorem	suborr2-P4.RC 561	Inference Form of suborr2-P4 560. †
⊢ (𝜒 ∨ 𝜑)    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜒 ∨ 𝜓)
Theorem	subord2-P4 562	Alternate Form of subord-P3.43c 350. †
⊢ (𝛾 → (𝜑 ∨ 𝜒))    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    &   ⊢ (𝛾 → (𝜒 ↔ 𝜗))    ⇒   ⊢ (𝛾 → (𝜓 ∨ 𝜗))
Theorem	subord2-P4.RC 563	Inference Form of subord2-P4 562. †
⊢ (𝜑 ∨ 𝜒)    &   ⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜗)    ⇒   ⊢ (𝜓 ∨ 𝜗)
5.4.7  More Convenient Forms for Commutivity Laws.
Theorem	andcomm2-P4 564	Alternate Form of andcomm-P3.35 314. †
⊢ (𝛾 → (𝜑 ∧ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 ∧ 𝜑))
Theorem	andcomm2-P4.RC 565	Inference Form of andcomm2-P4 564. †
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜓 ∧ 𝜑)
Theorem	orcomm2-P4 566	Alternate Form of orcomm-P3.37 319. †
⊢ (𝛾 → (𝜑 ∨ 𝜓))    ⇒   ⊢ (𝛾 → (𝜓 ∨ 𝜑))
Theorem	orcomm2-P4.RC 567	Inference Form of orcomm2-P4 566. †
⊢ (𝜑 ∨ 𝜓)    ⇒   ⊢ (𝜓 ∨ 𝜑)
5.4.8  More Convenient Forms for Associativity Laws.
Theorem	andassoc2a-P4 568	Alternate Form A of andassoc-P3.36 317. †
⊢ (𝛾 → ((𝜑 ∧ 𝜓) ∧ 𝜒))    ⇒   ⊢ (𝛾 → (𝜑 ∧ (𝜓 ∧ 𝜒)))
Theorem	andassoc2a-P4.RC 569	Inference Form of andassoc2a-P4 568. †
⊢ ((𝜑 ∧ 𝜓) ∧ 𝜒)    ⇒   ⊢ (𝜑 ∧ (𝜓 ∧ 𝜒))
Theorem	andassoc2b-P4 570	Alternate Form B of andassoc-P3.36 317. †
⊢ (𝛾 → (𝜑 ∧ (𝜓 ∧ 𝜒)))    ⇒   ⊢ (𝛾 → ((𝜑 ∧ 𝜓) ∧ 𝜒))
Theorem	andassoc2b-P4.RC 571	Inference Form of andassoc2b-P4 570. †
⊢ (𝜑 ∧ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) ∧ 𝜒)
Theorem	orassoc2a-P4 572	Alternate Form A of orassoc-P3.38 322. †
⊢ (𝛾 → ((𝜑 ∨ 𝜓) ∨ 𝜒))    ⇒   ⊢ (𝛾 → (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	orassoc2a-P4.RC 573	Inference Form of orassoc2a-P4 572. †
⊢ ((𝜑 ∨ 𝜓) ∨ 𝜒)    ⇒   ⊢ (𝜑 ∨ (𝜓 ∨ 𝜒))
Theorem	orassoc2b-P4 574	Alternate Form B of orassoc-P3.38 322. †
⊢ (𝛾 → (𝜑 ∨ (𝜓 ∨ 𝜒)))    ⇒   ⊢ (𝛾 → ((𝜑 ∨ 𝜓) ∨ 𝜒))
Theorem	orassoc2b-P4.RC 575	Inference Form of orassoc2b-P4 574. †
⊢ (𝜑 ∨ (𝜓 ∨ 𝜒))    ⇒   ⊢ ((𝜑 ∨ 𝜓) ∨ 𝜒)
5.4.9  More Convenient Forms for Joining Implications.
Theorem	joinimandinc2-P4 576	Alternate form of joinimandinc-P4.8a 397. †
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜒 → 𝜗))    ⇒   ⊢ (𝛾 → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜗)))
Theorem	joinimandinc2-P4.RC 577	Inference Form of joinimandinc2-P4 576. †
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜗)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜗))
Theorem	joinimandinc3-P4 578	Alternate form of joinimandinc-P4.8a 397. †
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜒 → 𝜓))    ⇒   ⊢ (𝛾 → ((𝜑 ∨ 𝜒) → 𝜓))
Theorem	joinimandinc3-P4.RC 579	Inference Form of joinimandinc3-P4 578. †
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → 𝜓)
Theorem	joinimandres2-P4 580	Alternate form of joinimandres-P4.8b 400. †
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜒 → 𝜗))    ⇒   ⊢ (𝛾 → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜗)))
Theorem	joinimandres2-P4.RC 581	Inference Form of joinimandres2-P4 580. †
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜗)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜗))
Theorem	joinimandres3-P4 582	Alternate form of joinimandres-P4.8b 400. †
⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → (𝜑 → 𝜒))    ⇒   ⊢ (𝛾 → (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	joinimandres3-P4.RC 583	Inference Form of joinimandres3-P4 582. †
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	joinimor2-P4 584	Alternate form of joinimor-P4.8c 403. †
⊢ (𝛾 → ((𝜑 → 𝜓) ∨ (𝜒 → 𝜓)))    ⇒   ⊢ (𝛾 → ((𝜑 ∧ 𝜒) → 𝜓))
Theorem	joinimor2-P4.RC 585	Inference Form of joinimor2-P4 584. †
⊢ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜓))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
Theorem	joinimor3-P4 586	Alternate form of joinimor-P4.8c 403. †
⊢ (𝛾 → ((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)))    ⇒   ⊢ (𝛾 → (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	joinimor3-P4.RC 587	Inference Form of joinimor3-P4 586. †
⊢ ((𝜑 → 𝜓) ∨ (𝜑 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ∨ 𝜒))
PART 6  Chapter 5: Predicate Calculus (FOL Axioms)
6.1  Consequences of ax-GEN and ax-L4.
6.1.1  The Universal Quantifier.
Theorem	alloverim-P5 588	'∀𝑥' Distributes Over '→'. This is the deductive form of ax-L4 16.
⊢ (𝛾 → ∀𝑥(𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alloverim-P5.RC 589	Inference Form of alloverim-P5 588.
⊢ ∀𝑥(𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	dalloverim-P5 590	Double '∀𝑥' Distribution Over '→'.
⊢ (𝛾 → ∀𝑥(𝜑 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)))
Theorem	dalloverim-P5.RC 591	Inference Form of dalloverim-P5 590.
⊢ ∀𝑥(𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
6.1.1.1  Generalization Augmentation.
Theorem	alloverim-P5.RC.GEN 592	Inference Form of alloverim-P5 588 with Generalization. For the deductive form with a variable restriction see alloverim-P5.GENV 621. For the most general form, see alloverim-P5.GENF 747.
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	dalloverim-P5.RC.GEN 593	Inference Form of dalloverim-P5 590 with generalization.
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))
6.1.1.2  A Substitution Law for Universal Quantification.
Theorem	suballinf-P5 594	Inference Version of '∀𝑥' Substitution Law. For the deductive form with a variable restriction, see suballv-P5 623. For the most general form, see suball-P6 753.
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)
6.1.2  The Existential Quantifier.
6.1.2.1  Syntax Definition.
Syntax	wff-exists 595	Extend WFF definition to include the existential quantifier '∃'.
wff ∃𝑥𝜑
6.1.2.2  Formal Definition.
Definition	df-exists-D5.1 596	Definition of Existential Quantifier, '∃'. Read as "there exists".
⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6.1.3  Dual Properties of Universal / Existential Quantification.
Theorem	allnegex-P5 597	"For all not" is Equivalent to "Does not exist". Dual of exnegall-P5 598.
⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
Theorem	exnegall-P5 598	"Exists a negative" is Equivalent to "Not for all". Dual of allnegex-P5 597.
⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Theorem	allasex-P5 599	Universal Quantification in Terms of Existential Quantification. Dual of df-exists-D5.1 596.
⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
Theorem	lemma-L5.01a 600	Transpositional Quantifier Equivalence Lemma.
⊢ ((∃𝑥𝜑 → 𝜑) ↔ (¬ 𝜑 → ∀𝑥 ¬ 𝜑))