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

Metamath Proof Explorer

Theorem ifbothda

Description: A wff th containing a conditional operator is true when both of its cases are true. (Contributed by NM, 15-Feb-2015)

Ref Expression
Hypotheses ifboth.1 
|- ( A = if ( ph , A , B ) -> ( ps <-> th ) )
ifboth.2 
|- ( B = if ( ph , A , B ) -> ( ch <-> th ) )
ifbothda.3 
|- ( ( et /\ ph ) -> ps )
ifbothda.4 
|- ( ( et /\ -. ph ) -> ch )
Assertion ifbothda 
|- ( et -> th )

Proof

Step Hyp Ref Expression
1 ifboth.1 
 |-  ( A = if ( ph , A , B ) -> ( ps <-> th ) )
2 ifboth.2 
 |-  ( B = if ( ph , A , B ) -> ( ch <-> th ) )
3 ifbothda.3 
 |-  ( ( et /\ ph ) -> ps )
4 ifbothda.4 
 |-  ( ( et /\ -. ph ) -> ch )
5 iftrue 
 |-  ( ph -> if ( ph , A , B ) = A )
6 5 eqcomd 
 |-  ( ph -> A = if ( ph , A , B ) )
7 6 1 syl 
 |-  ( ph -> ( ps <-> th ) )
8 7 adantl 
 |-  ( ( et /\ ph ) -> ( ps <-> th ) )
9 3 8 mpbid 
 |-  ( ( et /\ ph ) -> th )
10 iffalse 
 |-  ( -. ph -> if ( ph , A , B ) = B )
11 10 eqcomd 
 |-  ( -. ph -> B = if ( ph , A , B ) )
12 11 2 syl 
 |-  ( -. ph -> ( ch <-> th ) )
13 12 adantl 
 |-  ( ( et /\ -. ph ) -> ( ch <-> th ) )
14 4 13 mpbid 
 |-  ( ( et /\ -. ph ) -> th )
15 9 14 pm2.61dan 
 |-  ( et -> th )