# Metamath Proof Explorer

## Theorem ifpimimb

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

Ref Expression
Assertion ifpimimb ${⊢}if-\left({\phi },\left({\psi }\to {\chi }\right),\left({\theta }\to {\tau }\right)\right)↔\left(if-\left({\phi },{\psi },{\theta }\right)\to if-\left({\phi },{\chi },{\tau }\right)\right)$

### Proof

Step Hyp Ref Expression
1 dfifp2 ${⊢}if-\left({\phi },\left({\psi }\to {\chi }\right),\left({\theta }\to {\tau }\right)\right)↔\left(\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\wedge \left(¬{\phi }\to \left({\theta }\to {\tau }\right)\right)\right)$
2 imor ${⊢}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)↔\left(¬{\phi }\vee \left({\psi }\to {\chi }\right)\right)$
3 pm4.8 ${⊢}\left({\phi }\to ¬{\phi }\right)↔¬{\phi }$
4 3 bicomi ${⊢}¬{\phi }↔\left({\phi }\to ¬{\phi }\right)$
5 4 orbi1i ${⊢}\left(¬{\phi }\vee \left({\psi }\to {\chi }\right)\right)↔\left(\left({\phi }\to ¬{\phi }\right)\vee \left({\psi }\to {\chi }\right)\right)$
6 id ${⊢}{\phi }\to {\phi }$
7 6 orci ${⊢}\left(\left({\phi }\to {\phi }\right)\vee \left({\theta }\to {\chi }\right)\right)$
8 7 biantru ${⊢}\left(\left({\phi }\to ¬{\phi }\right)\vee \left({\psi }\to {\chi }\right)\right)↔\left(\left(\left({\phi }\to ¬{\phi }\right)\vee \left({\psi }\to {\chi }\right)\right)\wedge \left(\left({\phi }\to {\phi }\right)\vee \left({\theta }\to {\chi }\right)\right)\right)$
9 2 5 8 3bitri ${⊢}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)↔\left(\left(\left({\phi }\to ¬{\phi }\right)\vee \left({\psi }\to {\chi }\right)\right)\wedge \left(\left({\phi }\to {\phi }\right)\vee \left({\theta }\to {\chi }\right)\right)\right)$
10 pm4.64 ${⊢}\left(¬{\phi }\to \left({\theta }\to {\tau }\right)\right)↔\left({\phi }\vee \left({\theta }\to {\tau }\right)\right)$
11 pm4.81 ${⊢}\left(¬{\phi }\to {\phi }\right)↔{\phi }$
12 11 bicomi ${⊢}{\phi }↔\left(¬{\phi }\to {\phi }\right)$
13 12 orbi1i ${⊢}\left({\phi }\vee \left({\theta }\to {\tau }\right)\right)↔\left(\left(¬{\phi }\to {\phi }\right)\vee \left({\theta }\to {\tau }\right)\right)$
14 6 orci ${⊢}\left(\left({\phi }\to {\phi }\right)\vee \left({\psi }\to {\tau }\right)\right)$
15 14 biantrur ${⊢}\left(\left(¬{\phi }\to {\phi }\right)\vee \left({\theta }\to {\tau }\right)\right)↔\left(\left(\left({\phi }\to {\phi }\right)\vee \left({\psi }\to {\tau }\right)\right)\wedge \left(\left(¬{\phi }\to {\phi }\right)\vee \left({\theta }\to {\tau }\right)\right)\right)$
16 10 13 15 3bitri ${⊢}\left(¬{\phi }\to \left({\theta }\to {\tau }\right)\right)↔\left(\left(\left({\phi }\to {\phi }\right)\vee \left({\psi }\to {\tau }\right)\right)\wedge \left(\left(¬{\phi }\to {\phi }\right)\vee \left({\theta }\to {\tau }\right)\right)\right)$
17 9 16 anbi12i ${⊢}\left(\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\wedge \left(¬{\phi }\to \left({\theta }\to {\tau }\right)\right)\right)↔\left(\left(\left(\left({\phi }\to ¬{\phi }\right)\vee \left({\psi }\to {\chi }\right)\right)\wedge \left(\left({\phi }\to {\phi }\right)\vee \left({\theta }\to {\chi }\right)\right)\right)\wedge \left(\left(\left({\phi }\to {\phi }\right)\vee \left({\psi }\to {\tau }\right)\right)\wedge \left(\left(¬{\phi }\to {\phi }\right)\vee \left({\theta }\to {\tau }\right)\right)\right)\right)$
18 ifpim123g ${⊢}\left(if-\left({\phi },{\psi },{\theta }\right)\to if-\left({\phi },{\chi },{\tau }\right)\right)↔\left(\left(\left(\left({\phi }\to ¬{\phi }\right)\vee \left({\psi }\to {\chi }\right)\right)\wedge \left(\left({\phi }\to {\phi }\right)\vee \left({\theta }\to {\chi }\right)\right)\right)\wedge \left(\left(\left({\phi }\to {\phi }\right)\vee \left({\psi }\to {\tau }\right)\right)\wedge \left(\left(¬{\phi }\to {\phi }\right)\vee \left({\theta }\to {\tau }\right)\right)\right)\right)$
19 18 bicomi ${⊢}\left(\left(\left(\left({\phi }\to ¬{\phi }\right)\vee \left({\psi }\to {\chi }\right)\right)\wedge \left(\left({\phi }\to {\phi }\right)\vee \left({\theta }\to {\chi }\right)\right)\right)\wedge \left(\left(\left({\phi }\to {\phi }\right)\vee \left({\psi }\to {\tau }\right)\right)\wedge \left(\left(¬{\phi }\to {\phi }\right)\vee \left({\theta }\to {\tau }\right)\right)\right)\right)↔\left(if-\left({\phi },{\psi },{\theta }\right)\to if-\left({\phi },{\chi },{\tau }\right)\right)$
20 1 17 19 3bitri ${⊢}if-\left({\phi },\left({\psi }\to {\chi }\right),\left({\theta }\to {\tau }\right)\right)↔\left(if-\left({\phi },{\psi },{\theta }\right)\to if-\left({\phi },{\chi },{\tau }\right)\right)$