Metamath Proof Explorer


Theorem ifpororb

Description: Factor conditional logic operator over disjunction in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

Ref Expression
Assertion ifpororb ( if- ( 𝜑 , ( 𝜓𝜒 ) , ( 𝜃𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )

Proof

Step Hyp Ref Expression
1 dfifp2 ( if- ( 𝜑 , ( 𝜓𝜒 ) , ( 𝜃𝜏 ) ) ↔ ( ( 𝜑 → ( 𝜓𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃𝜏 ) ) ) )
2 df-or ( ( 𝜓𝜒 ) ↔ ( ¬ 𝜓𝜒 ) )
3 2 imbi2i ( ( 𝜑 → ( 𝜓𝜒 ) ) ↔ ( 𝜑 → ( ¬ 𝜓𝜒 ) ) )
4 df-or ( ( 𝜃𝜏 ) ↔ ( ¬ 𝜃𝜏 ) )
5 4 imbi2i ( ( ¬ 𝜑 → ( 𝜃𝜏 ) ) ↔ ( ¬ 𝜑 → ( ¬ 𝜃𝜏 ) ) )
6 3 5 anbi12i ( ( ( 𝜑 → ( 𝜓𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃𝜏 ) ) ) ↔ ( ( 𝜑 → ( ¬ 𝜓𝜒 ) ) ∧ ( ¬ 𝜑 → ( ¬ 𝜃𝜏 ) ) ) )
7 ifpimimb ( if- ( 𝜑 , ( ¬ 𝜓𝜒 ) , ( ¬ 𝜃𝜏 ) ) ↔ ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
8 dfifp2 ( if- ( 𝜑 , ( ¬ 𝜓𝜒 ) , ( ¬ 𝜃𝜏 ) ) ↔ ( ( 𝜑 → ( ¬ 𝜓𝜒 ) ) ∧ ( ¬ 𝜑 → ( ¬ 𝜃𝜏 ) ) ) )
9 imor ( ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( ¬ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
10 ifpnot23d ( ¬ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ↔ if- ( 𝜑 , 𝜓 , 𝜃 ) )
11 10 orbi1i ( ( ¬ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
12 9 11 bitri ( ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
13 7 8 12 3bitr3i ( ( ( 𝜑 → ( ¬ 𝜓𝜒 ) ) ∧ ( ¬ 𝜑 → ( ¬ 𝜃𝜏 ) ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
14 1 6 13 3bitri ( if- ( 𝜑 , ( 𝜓𝜒 ) , ( 𝜃𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )