Theorem wl-2mintru1

Description: Using the recursion formula

"(n+1)-mintru-(m+1)" <-> if- ( ph , "n-mintru-m" , "n-mintru-(m+1)" )

for "2-mintru-1" (meaning "at least 1 out of 2 inputs is true") by plugging in n = 1, m = 0, and simplifying. The expression "1-mintru-0" is a base case (meaning at least zero inputs out of 1 are true), evaluating to T. , and wl-1mintru1 shows "1-mintru-1" is equivalent to the only input.

Negating an "n-mintru1" operation means: All n inputs ph .. th are false. This is also conveniently expressed as -. ( ph \/ .. \/ th ) , in accordance with the result here. (Contributed by Wolf Lammen, 10-May-2024)

	Ref	Expression
Assertion	wl-2mintru1	$$⊢if-\left(\psi ,\top ,\chi \right)\leftrightarrow \left(\psi \vee \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dfifp3	$$⊢if-\left(\psi ,\top ,\chi \right)\leftrightarrow \left(\left(\psi \to \top \right)\wedge \left(\psi \vee \chi \right)\right)$$
2		trud	$$⊢\psi \to \top$$
3	2	bitru	$$⊢\left(\psi \to \top \right)\leftrightarrow \top$$
4	3	anbi1i	$$⊢\left(\left(\psi \to \top \right)\wedge \left(\psi \vee \chi \right)\right)\leftrightarrow \left(\top \wedge \left(\psi \vee \chi \right)\right)$$
5		truan	$$⊢\left(\top \wedge \left(\psi \vee \chi \right)\right)\leftrightarrow \left(\psi \vee \chi \right)$$
6	1 4 5	3bitri	$$⊢if-\left(\psi ,\top ,\chi \right)\leftrightarrow \left(\psi \vee \chi \right)$$