Metamath Proof Explorer


Theorem noranOLD

Description: Obsolete version of noran as of 8-Dec-2023. (Contributed by Remi, 26-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion noranOLD ( ( 𝜑𝜓 ) ↔ ( ( 𝜑 𝜑 ) ( 𝜓 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 ianor ( ¬ ( 𝜑𝜓 ) ↔ ( ¬ 𝜑 ∨ ¬ 𝜓 ) )
2 1 notbii ( ¬ ¬ ( 𝜑𝜓 ) ↔ ¬ ( ¬ 𝜑 ∨ ¬ 𝜓 ) )
3 nornot ( ¬ 𝜑 ↔ ( 𝜑 𝜑 ) )
4 nornot ( ¬ 𝜓 ↔ ( 𝜓 𝜓 ) )
5 3 4 orbi12i ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) ↔ ( ( 𝜑 𝜑 ) ∨ ( 𝜓 𝜓 ) ) )
6 5 notbii ( ¬ ( ¬ 𝜑 ∨ ¬ 𝜓 ) ↔ ¬ ( ( 𝜑 𝜑 ) ∨ ( 𝜓 𝜓 ) ) )
7 ioran ( ¬ ( ( 𝜑 𝜑 ) ∨ ( 𝜓 𝜓 ) ) ↔ ( ¬ ( 𝜑 𝜑 ) ∧ ¬ ( 𝜓 𝜓 ) ) )
8 2 6 7 3bitrri ( ( ¬ ( 𝜑 𝜑 ) ∧ ¬ ( 𝜓 𝜓 ) ) ↔ ¬ ¬ ( 𝜑𝜓 ) )
9 df-nor ( ( ( 𝜑 𝜑 ) ( 𝜓 𝜓 ) ) ↔ ¬ ( ( 𝜑 𝜑 ) ∨ ( 𝜓 𝜓 ) ) )
10 9 7 bitri ( ( ( 𝜑 𝜑 ) ( 𝜓 𝜓 ) ) ↔ ( ¬ ( 𝜑 𝜑 ) ∧ ¬ ( 𝜓 𝜓 ) ) )
11 notnotb ( ( 𝜑𝜓 ) ↔ ¬ ¬ ( 𝜑𝜓 ) )
12 8 10 11 3bitr4ri ( ( 𝜑𝜓 ) ↔ ( ( 𝜑 𝜑 ) ( 𝜓 𝜓 ) ) )