P. 435 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43401-43500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fpwfvss 43401	Functions into a powerset always have values which are subsets. This is dependant on our convention when the argument is not part of the domain. (Contributed by RP, 13-Sep-2024.)
⊢ 𝐹:𝐶⟶𝒫 𝐵    ⇒   ⊢ (𝐹‘𝐴) ⊆ 𝐵
Theorem	sdomne0 43402	A class that strictly dominates any set is not empty. (Suggested by SN, 14-Jan-2025.) (Contributed by RP, 14-Jan-2025.)
⊢ (𝐵 ≺ 𝐴 → 𝐴 ≠ ∅)
Theorem	sdomne0d 43403	A class that strictly dominates any set is not empty. (Contributed by RP, 3-Sep-2024.)
⊢ (𝜑 → 𝐵 ≺ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐴 ≠ ∅)
Theorem	safesnsupfiss 43404	If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.)
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ⊆ 𝐵)
Theorem	safesnsupfiub 43405*	If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.)
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑥𝑅𝑦)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)∀𝑦 ∈ 𝐶 𝑥𝑅𝑦)
Theorem	safesnsupfidom1o 43406	If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 1-Sep-2024.)
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o)
Theorem	safesnsupfilb 43407*	If 𝐵 is a finite subset of ordered class 𝐴, we can safely create a small subset with the same largest element and upper bound, if any. (Contributed by RP, 3-Sep-2024.)
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o))    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑅 Or 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦)
Theorem	isoeq145d 43408	Equality deduction for isometries. (Contributed by RP, 14-Jan-2025.)
⊢ (𝜑 → 𝐹 = 𝐺)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → (𝐹 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐶, 𝐷)))
Theorem	resisoeq45d 43409	Equality deduction for equally restricted isometries. (Contributed by RP, 14-Jan-2025.)
⊢ (𝜑 → 𝐴 = 𝐶)    &   ⊢ (𝜑 → 𝐵 = 𝐷)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ 𝐴) Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐹 ↾ 𝐶) Isom 𝑅, 𝑆 (𝐶, 𝐷)))
Theorem	negslem1 43410	An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024.)
⊢ (𝐴 = 𝐵 → ((𝐹 ↾ 𝐴) Isom 𝑅, ◡𝑅(𝐴, 𝐴) ↔ (𝐹 ↾ 𝐵) Isom 𝑅, ◡𝑅(𝐵, 𝐵)))
Theorem	nvocnvb 43411*	Equivalence to saying the converse of an involution is the function itself. (Contributed by RP, 13-Oct-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 = 𝐹) ↔ (𝐹:𝐴–1-1-onto→𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘(𝐹‘𝑥)) = 𝑥))
Theorem	rp-brsslt 43412*	Binary relation form of a relation, <, which has been extended from relation 𝑅 to subsets of class 𝑆. Usually, we will assume 𝑅 Or 𝑆. Definition in [Alling], p. 2. Generalization of brsslt 27844. (Originally by Scott Fenton, 8-Dec-2021.) (Contributed by RP, 28-Nov-2023.)
⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)}    ⇒   ⊢ (𝐴 < 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝑥𝑅𝑦)))
Theorem	nla0002 43413*	Extending a linear order to subsets, the empty set is less than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.)
⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)}    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → ∅ < 𝐴)
Theorem	nla0003 43414*	Extending a linear order to subsets, the empty set is greater than any subset. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.)
⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)}    &   ⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑆)    ⇒   ⊢ (𝜑 → 𝐴 < ∅)
Theorem	nla0001 43415*	Extending a linear order to subsets, the empty set is less than itself. Note in [Alling], p. 3. (Contributed by RP, 28-Nov-2023.)
⊢ < = {⟨𝑎, 𝑏⟩ ∣ (𝑎 ⊆ 𝑆 ∧ 𝑏 ⊆ 𝑆 ∧ ∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 𝑥𝑅𝑦)}    ⇒   ⊢ (𝜑 → ∅ < ∅)
Theorem	faosnf0.11b 43416*	𝐵 is called a non-limit ordinal if it is not a limit ordinal. (Contributed by RP, 27-Sep-2023.) Alling, Norman L. "Fundamentals of Analysis Over Surreal Numbers Fields." The Rocky Mountain Journal of Mathematics 19, no. 3 (1989): 565-73. http://www.jstor.org/stable/44237243.
⊢ ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)
Theorem	dfno2 43417	A surreal number, in the functional sign expansion representation, is a function which maps from an ordinal into a set of two possible signs. (Contributed by RP, 12-Jan-2025.)
⊢ No = {𝑓 ∈ 𝒫 (On × {1o, 2o}) ∣ (Fun 𝑓 ∧ dom 𝑓 ∈ On)}
Theorem	onnog 43418	Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → (𝐴 × {𝐵}) ∈ No )
Theorem	onnobdayg 43419	Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ {1o, 2o}) → ( bday ‘(𝐴 × {𝐵})) = 𝐴)
Theorem	bdaybndex 43420	Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023.)
⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → (𝐵 × {𝐶}) ∈ No )
Theorem	bdaybndbday 43421	Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023.)
⊢ ((𝐴 ∈ No ∧ 𝐵 = ( bday ‘𝐴) ∧ 𝐶 ∈ {1o, 2o}) → ( bday ‘(𝐵 × {𝐶})) = ( bday ‘𝐴))
Theorem	onno 43422	Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (𝐴 ∈ On → (𝐴 × {2o}) ∈ No )
Theorem	onnoi 43423	Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ 𝐴 ∈ On    ⇒   ⊢ (𝐴 × {2o}) ∈ No
Theorem	0no 43424	Ordinal zero maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ ∅ ∈ No
Theorem	1no 43425	Ordinal one maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (1o × {2o}) ∈ No
Theorem	2no 43426	Ordinal two maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (2o × {2o}) ∈ No
Theorem	3no 43427	Ordinal three maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (3o × {2o}) ∈ No
Theorem	4no 43428	Ordinal four maps to a surreal number. (Contributed by RP, 21-Sep-2023.)
⊢ (4o × {2o}) ∈ No
Theorem	fnimafnex 43429	The functional image of a function value exists. (Contributed by RP, 31-Oct-2024.)
⊢ 𝐹 Fn 𝐵    ⇒   ⊢ (𝐹 “ (𝐺‘𝐴)) ∈ V
21.36.4  Short Studies
Theorem	nlimsuc 43430	A successor is not a limit ordinal. (Contributed by RP, 13-Dec-2024.)
⊢ (𝐴 ∈ On → ¬ Lim suc 𝐴)
Theorem	nlim1NEW 43431	1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.)
⊢ ¬ Lim 1o
Theorem	nlim2NEW 43432	2 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024.) (Proof shortened by RP, 13-Dec-2024.)
⊢ ¬ Lim 2o
Theorem	nlim3 43433	3 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.)
⊢ ¬ Lim 3o
Theorem	nlim4 43434	4 is not a limit ordinal. (Contributed by RP, 13-Dec-2024.)
⊢ ¬ Lim 4o
Theorem	oa1un 43435	Given 𝐴 ∈ On, let 𝐴 +o 1o be defined to be the union of 𝐴 and {𝐴}. Compare with oa1suc 8567. (Contributed by RP, 27-Sep-2023.)
⊢ (𝐴 ∈ On → (𝐴 +o 1o) = (𝐴 ∪ {𝐴}))
Theorem	oa1cl 43436	𝐴 +o 1o is in On. (Contributed by RP, 27-Sep-2023.)
⊢ (𝐴 ∈ On → (𝐴 +o 1o) ∈ On)
Theorem	0finon 43437	0 is a finite ordinal. See peano1 7910. (Contributed by RP, 27-Sep-2023.)
⊢ ∅ ∈ (On ∩ Fin)
Theorem	1finon 43438	1 is a finite ordinal. See 1onn 8676. (Contributed by RP, 27-Sep-2023.)
⊢ 1o ∈ (On ∩ Fin)
Theorem	2finon 43439	2 is a finite ordinal. See 1onn 8676. (Contributed by RP, 27-Sep-2023.)
⊢ 2o ∈ (On ∩ Fin)
Theorem	3finon 43440	3 is a finite ordinal. See 1onn 8676. (Contributed by RP, 27-Sep-2023.)
⊢ 3o ∈ (On ∩ Fin)
Theorem	4finon 43441	4 is a finite ordinal. See 1onn 8676. (Contributed by RP, 27-Sep-2023.)
⊢ 4o ∈ (On ∩ Fin)
Theorem	finona1cl 43442	The finite ordinals are closed under the add one operation. (Contributed by RP, 27-Sep-2023.)
⊢ (𝑁 ∈ (On ∩ Fin) → (𝑁 +o 1o) ∈ (On ∩ Fin))
Theorem	finonex 43443	The finite ordinals are a set. See also onprc 7796 and fiprc 9083 for proof that On and Fin are proper classes. (Contributed by RP, 27-Sep-2023.)
⊢ (On ∩ Fin) ∈ V
Theorem	fzunt 43444	Union of two adjacent finite sets of sequential integers that share a common endpoint. (Suggested by NM, 21-Jul-2005.) (Contributed by RP, 14-Dec-2024.)
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
Theorem	fzuntd 43445	Union of two adjacent finite sets of sequential integers that share a common endpoint. (Contributed by RP, 14-Dec-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐾...𝑀) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
Theorem	fzunt1d 43446	Union of two overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑀 ≤ 𝐿)    &   ⊢ (𝜑 → 𝐿 ≤ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
Theorem	fzuntgd 43447	Union of two adjacent or overlapping finite sets of sequential integers. (Contributed by RP, 14-Dec-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝐿 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ≤ 𝑀)    &   ⊢ (𝜑 → 𝑀 ≤ (𝐿 + 1))    &   ⊢ (𝜑 → 𝐿 ≤ 𝑁)    ⇒   ⊢ (𝜑 → ((𝐾...𝐿) ∪ (𝑀...𝑁)) = (𝐾...𝑁))
21.36.4.1  Additional work on conditional logical operator
Theorem	ifpan123g 43448	Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) ∧ if-(𝜓, 𝜃, 𝜂)) ↔ (((¬ 𝜑 ∨ 𝜒) ∧ (𝜑 ∨ 𝜏)) ∧ ((¬ 𝜓 ∨ 𝜃) ∧ (𝜓 ∨ 𝜂))))
Theorem	ifpan23 43449	Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.)
⊢ ((if-(𝜑, 𝜓, 𝜒) ∧ if-(𝜑, 𝜃, 𝜏)) ↔ if-(𝜑, (𝜓 ∧ 𝜃), (𝜒 ∧ 𝜏)))
Theorem	ifpdfor2 43450	Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, 𝜑, 𝜓))
Theorem	ifporcor 43451	Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.)
⊢ (if-(𝜑, 𝜑, 𝜓) ↔ if-(𝜓, 𝜓, 𝜑))
Theorem	ifpdfan2 43452	Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, 𝜑))
Theorem	ifpancor 43453	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜓, 𝜑) ↔ if-(𝜓, 𝜑, 𝜓))
Theorem	ifpdfor 43454	Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∨ 𝜓) ↔ if-(𝜑, ⊤, 𝜓))
Theorem	ifpdfan 43455	Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ∧ 𝜓) ↔ if-(𝜑, 𝜓, ⊥))
Theorem	ifpbi2 43456	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜑, 𝜃) ↔ if-(𝜒, 𝜓, 𝜃)))
Theorem	ifpbi3 43457	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜒, 𝜃, 𝜑) ↔ if-(𝜒, 𝜃, 𝜓)))
Theorem	ifpim1 43458	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(¬ 𝜑, ⊤, 𝜓))
Theorem	ifpnot 43459	Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ (¬ 𝜑 ↔ if-(𝜑, ⊥, ⊤))
Theorem	ifpid2 43460	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ (𝜑 ↔ if-(𝜑, ⊤, ⊥))
Theorem	ifpim2 43461	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, ⊤, ¬ 𝜑))
Theorem	ifpbi23 43462	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜏, 𝜑, 𝜒) ↔ if-(𝜏, 𝜓, 𝜃)))
Theorem	ifpbiidcor 43463	Restatement of biid 261. (Contributed by RP, 25-Apr-2020.)
⊢ if-(𝜑, 𝜑, ¬ 𝜑)
Theorem	ifpbicor 43464	Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜓, ¬ 𝜓) ↔ if-(𝜓, 𝜑, ¬ 𝜑))
Theorem	ifpxorcor 43465	Corollary of commutation of biconditional. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, 𝜓) ↔ if-(𝜓, ¬ 𝜑, 𝜑))
Theorem	ifpbi1 43466	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
⊢ ((𝜑 ↔ 𝜓) → (if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)))
Theorem	ifpnot23 43467	Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.)
⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒))
Theorem	ifpnotnotb 43468	Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ¬ if-(𝜑, 𝜓, 𝜒))
Theorem	ifpnorcor 43469	Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜑, ¬ 𝜓) ↔ if-(𝜓, ¬ 𝜓, ¬ 𝜑))
Theorem	ifpnancor 43470	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜑) ↔ if-(𝜓, ¬ 𝜑, ¬ 𝜓))
Theorem	ifpnot23b 43471	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, ¬ 𝜓, 𝜒) ↔ if-(𝜑, 𝜓, ¬ 𝜒))
Theorem	ifpbiidcor2 43472	Restatement of biid 261. (Contributed by RP, 25-Apr-2020.)
⊢ ¬ if-(𝜑, ¬ 𝜑, 𝜑)
Theorem	ifpnot23c 43473	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, 𝜓, ¬ 𝜒) ↔ if-(𝜑, ¬ 𝜓, 𝜒))
Theorem	ifpnot23d 43474	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ if-(𝜑, 𝜓, 𝜒))
Theorem	ifpdfnan 43475	Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ⊼ 𝜓) ↔ if-(𝜑, ¬ 𝜓, ⊤))
Theorem	ifpdfxor 43476	Define xor as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ⊻ 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜓))
Theorem	ifpbi12 43477	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜏)))
Theorem	ifpbi13 43478	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → (if-(𝜑, 𝜏, 𝜒) ↔ if-(𝜓, 𝜏, 𝜃)))
Theorem	ifpbi123 43479	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (if-(𝜑, 𝜒, 𝜏) ↔ if-(𝜓, 𝜃, 𝜂)))
Theorem	ifpidg 43480	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜃 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((((𝜑 ∧ 𝜓) → 𝜃) ∧ ((𝜑 ∧ 𝜃) → 𝜓)) ∧ ((𝜒 → (𝜑 ∨ 𝜃)) ∧ (𝜃 → (𝜑 ∨ 𝜒)))))
Theorem	ifpid3g 43481	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜒 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝜓)))
Theorem	ifpid2g 43482	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜓 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜓 → (𝜑 ∨ 𝜒)) ∧ (𝜒 → (𝜑 ∨ 𝜓))))
Theorem	ifpid1g 43483	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((𝜑 ↔ if-(𝜑, 𝜓, 𝜒)) ↔ ((𝜒 → 𝜑) ∧ (𝜑 → 𝜓)))
Theorem	ifpim23g 43484	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (((𝜑 → 𝜓) ↔ if-(𝜒, 𝜓, ¬ 𝜑)) ↔ (((𝜑 ∧ 𝜓) → 𝜒) ∧ (𝜒 → (𝜑 ∨ 𝜓))))
Theorem	ifpim3 43485	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜑))
Theorem	ifpnim1 43486	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜑, ¬ 𝜓, 𝜑))
Theorem	ifpim4 43487	Restate implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ ((𝜑 → 𝜓) ↔ if-(𝜓, 𝜓, ¬ 𝜑))
Theorem	ifpnim2 43488	Restate negated implication as conditional logic operator. (Contributed by RP, 25-Apr-2020.)
⊢ (¬ (𝜑 → 𝜓) ↔ if-(𝜓, ¬ 𝜓, 𝜑))
Theorem	ifpim123g 43489	Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) → if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 → 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 → 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 → 𝜂)))))
Theorem	ifpim1g 43490	Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) → if-(𝜓, 𝜒, 𝜃)) ↔ (((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)) ∧ ((𝜑 → 𝜓) ∨ (𝜒 → 𝜃))))
Theorem	ifp1bi 43491	Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜃) ↔ if-(𝜓, 𝜒, 𝜃)) ↔ ((((𝜑 → 𝜓) ∨ (𝜒 → 𝜃)) ∧ ((𝜑 → 𝜓) ∨ (𝜃 → 𝜒))) ∧ (((𝜓 → 𝜑) ∨ (𝜒 → 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜃 → 𝜒)))))
Theorem	ifpbi1b 43492	When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020.)
⊢ (if-(𝜑, 𝜒, 𝜒) ↔ if-(𝜓, 𝜒, 𝜒))
Theorem	ifpimimb 43493	Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpororb 43494	Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∨ 𝜒), (𝜃 ∨ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∨ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpananb 43495	Factor conditional logic operator over conjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ∧ 𝜒), (𝜃 ∧ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ∧ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpnannanb 43496	Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊼ 𝜒), (𝜃 ⊼ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊼ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpor123g 43497	Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
⊢ ((if-(𝜑, 𝜒, 𝜏) ∨ if-(𝜓, 𝜃, 𝜂)) ↔ ((((𝜑 → ¬ 𝜓) ∨ (𝜒 ∨ 𝜃)) ∧ ((𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜃))) ∧ (((𝜑 → 𝜓) ∨ (𝜒 ∨ 𝜂)) ∧ ((¬ 𝜓 → 𝜑) ∨ (𝜏 ∨ 𝜂)))))
Theorem	ifpimim 43498	Consequnce of implication. (Contributed by RP, 17-Apr-2020.)
⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) → (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpbibib 43499	Factor conditional logic operator over biconditional in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ↔ 𝜒), (𝜃 ↔ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ↔ if-(𝜑, 𝜒, 𝜏)))
Theorem	ifpxorxorb 43500	Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
⊢ (if-(𝜑, (𝜓 ⊻ 𝜒), (𝜃 ⊻ 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) ⊻ if-(𝜑, 𝜒, 𝜏)))