This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ifpbi123d

Description: Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020) (Proof shortened by Wolf Lammen, 17-Apr-2024)

Ref Expression
Hypotheses ifpbi123d.1 
|- ( ph -> ( ps <-> ta ) )
ifpbi123d.2 
|- ( ph -> ( ch <-> et ) )
ifpbi123d.3 
|- ( ph -> ( th <-> ze ) )
Assertion ifpbi123d 
|- ( ph -> ( if- ( ps , ch , th ) <-> if- ( ta , et , ze ) ) )

Proof

Step Hyp Ref Expression
1 ifpbi123d.1 
 |-  ( ph -> ( ps <-> ta ) )
2 ifpbi123d.2 
 |-  ( ph -> ( ch <-> et ) )
3 ifpbi123d.3 
 |-  ( ph -> ( th <-> ze ) )
4 1 2 imbi12d 
 |-  ( ph -> ( ( ps -> ch ) <-> ( ta -> et ) ) )
5 1 3 orbi12d 
 |-  ( ph -> ( ( ps \/ th ) <-> ( ta \/ ze ) ) )
6 4 5 anbi12d 
 |-  ( ph -> ( ( ( ps -> ch ) /\ ( ps \/ th ) ) <-> ( ( ta -> et ) /\ ( ta \/ ze ) ) ) )
7 dfifp3 
 |-  ( if- ( ps , ch , th ) <-> ( ( ps -> ch ) /\ ( ps \/ th ) ) )
8 dfifp3 
 |-  ( if- ( ta , et , ze ) <-> ( ( ta -> et ) /\ ( ta \/ ze ) ) )
9 6 7 8 3bitr4g 
 |-  ( ph -> ( if- ( ps , ch , th ) <-> if- ( ta , et , ze ) ) )