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

Metamath Proof Explorer

Theorem ifan

Description: Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Assertion ifan 
|- if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B )

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( ph -> if ( ph , if ( ps , A , B ) , B ) = if ( ps , A , B ) )
2 ibar 
 |-  ( ph -> ( ps <-> ( ph /\ ps ) ) )
3 2 ifbid 
 |-  ( ph -> if ( ps , A , B ) = if ( ( ph /\ ps ) , A , B ) )
4 1 3 eqtr2d 
 |-  ( ph -> if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B ) )
5 simpl 
 |-  ( ( ph /\ ps ) -> ph )
6 5 con3i 
 |-  ( -. ph -> -. ( ph /\ ps ) )
7 6 iffalsed 
 |-  ( -. ph -> if ( ( ph /\ ps ) , A , B ) = B )
8 iffalse 
 |-  ( -. ph -> if ( ph , if ( ps , A , B ) , B ) = B )
9 7 8 eqtr4d 
 |-  ( -. ph -> if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B ) )
10 4 9 pm2.61i 
 |-  if ( ( ph /\ ps ) , A , B ) = if ( ph , if ( ps , A , B ) , B )