Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-dfif5ALT Structured version   Unicode version

Theorem bj-dfif5ALT 33863
Description: Alternate proof of bj-dfif5 33862 not using cases2 969. (Contributed by BJ, 5-Oct-2019.) Proof modification is discouraged to avoid use of cases2 969, but other shortenings are fine. (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
bj-dfif5ALT  |-  (if- (
ph ,  ps ,  ch )  <->  ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ch )
) )

Proof of Theorem bj-dfif5ALT
StepHypRef Expression
1 bj-dfif3 33860 . 2  |-  (if- (
ph ,  ps ,  ch )  <->  ( ( -. 
ph  \/  ps )  /\  ( ph  \/  ch ) ) )
2 anddi 868 . . 3  |-  ( ( ( -.  ph  \/  ps )  /\  ( ph  \/  ch ) )  <-> 
( ( ( -. 
ph  /\  ph )  \/  ( -.  ph  /\  ch ) )  \/  (
( ps  /\  ph )  \/  ( ps  /\ 
ch ) ) ) )
3 pm3.24 880 . . . . . . . . 9  |-  -.  ( ph  /\  -.  ph )
43pm2.21i 131 . . . . . . . 8  |-  ( (
ph  /\  -.  ph )  ->  ( -.  ph  /\  ch ) )
54ancoms 453 . . . . . . 7  |-  ( ( -.  ph  /\  ph )  ->  ( -.  ph  /\  ch ) )
65bj-jaoi1 33843 . . . . . 6  |-  ( ( ( -.  ph  /\  ph )  \/  ( -. 
ph  /\  ch )
)  ->  ( -.  ph 
/\  ch ) )
7 olc 384 . . . . . 6  |-  ( ( -.  ph  /\  ch )  ->  ( ( -.  ph  /\ 
ph )  \/  ( -.  ph  /\  ch )
) )
86, 7impbii 188 . . . . 5  |-  ( ( ( -.  ph  /\  ph )  \/  ( -. 
ph  /\  ch )
)  <->  ( -.  ph  /\ 
ch ) )
98orbi1i 520 . . . 4  |-  ( ( ( ( -.  ph  /\ 
ph )  \/  ( -.  ph  /\  ch )
)  \/  ( ( ps  /\  ph )  \/  ( ps  /\  ch ) ) )  <->  ( ( -.  ph  /\  ch )  \/  ( ( ps  /\  ph )  \/  ( ps 
/\  ch ) ) ) )
10 orc 385 . . . . . . 7  |-  ( ( -.  ph  /\  ch )  ->  ( ( -.  ph  /\ 
ch )  \/  ( ph  /\  ps ) ) )
11 olc 384 . . . . . . . . 9  |-  ( (
ph  /\  ps )  ->  ( ( -.  ph  /\ 
ch )  \/  ( ph  /\  ps ) ) )
1211ancoms 453 . . . . . . . 8  |-  ( ( ps  /\  ph )  ->  ( ( -.  ph  /\ 
ch )  \/  ( ph  /\  ps ) ) )
1311ex 434 . . . . . . . . . 10  |-  ( ph  ->  ( ps  ->  (
( -.  ph  /\  ch )  \/  ( ph  /\  ps ) ) ) )
1413adantrd 468 . . . . . . . . 9  |-  ( ph  ->  ( ( ps  /\  ch )  ->  ( ( -.  ph  /\  ch )  \/  ( ph  /\  ps ) ) ) )
1510ex 434 . . . . . . . . . 10  |-  ( -. 
ph  ->  ( ch  ->  ( ( -.  ph  /\  ch )  \/  ( ph  /\  ps ) ) ) )
1615adantld 467 . . . . . . . . 9  |-  ( -. 
ph  ->  ( ( ps 
/\  ch )  ->  (
( -.  ph  /\  ch )  \/  ( ph  /\  ps ) ) ) )
1714, 16pm2.61i 164 . . . . . . . 8  |-  ( ( ps  /\  ch )  ->  ( ( -.  ph  /\ 
ch )  \/  ( ph  /\  ps ) ) )
1812, 17jaoi 379 . . . . . . 7  |-  ( ( ( ps  /\  ph )  \/  ( ps  /\ 
ch ) )  -> 
( ( -.  ph  /\ 
ch )  \/  ( ph  /\  ps ) ) )
1910, 18jaoi 379 . . . . . 6  |-  ( ( ( -.  ph  /\  ch )  \/  (
( ps  /\  ph )  \/  ( ps  /\ 
ch ) ) )  ->  ( ( -. 
ph  /\  ch )  \/  ( ph  /\  ps ) ) )
20 pm1.4 386 . . . . . 6  |-  ( ( ( -.  ph  /\  ch )  \/  ( ph  /\  ps ) )  ->  ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ch )
) )
2119, 20syl 16 . . . . 5  |-  ( ( ( -.  ph  /\  ch )  \/  (
( ps  /\  ph )  \/  ( ps  /\ 
ch ) ) )  ->  ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ch )
) )
22 pm1.4 386 . . . . . 6  |-  ( ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ch ) )  -> 
( ( -.  ph  /\ 
ch )  \/  ( ph  /\  ps ) ) )
23 orc 385 . . . . . . . 8  |-  ( ( ps  /\  ph )  ->  ( ( ps  /\  ph )  \/  ( ps 
/\  ch ) ) )
2423ancoms 453 . . . . . . 7  |-  ( (
ph  /\  ps )  ->  ( ( ps  /\  ph )  \/  ( ps 
/\  ch ) ) )
2524orim2i 518 . . . . . 6  |-  ( ( ( -.  ph  /\  ch )  \/  ( ph  /\  ps ) )  ->  ( ( -. 
ph  /\  ch )  \/  ( ( ps  /\  ph )  \/  ( ps 
/\  ch ) ) ) )
2622, 25syl 16 . . . . 5  |-  ( ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ch ) )  -> 
( ( -.  ph  /\ 
ch )  \/  (
( ps  /\  ph )  \/  ( ps  /\ 
ch ) ) ) )
2721, 26impbii 188 . . . 4  |-  ( ( ( -.  ph  /\  ch )  \/  (
( ps  /\  ph )  \/  ( ps  /\ 
ch ) ) )  <-> 
( ( ph  /\  ps )  \/  ( -.  ph  /\  ch )
) )
289, 27bitri 249 . . 3  |-  ( ( ( ( -.  ph  /\ 
ph )  \/  ( -.  ph  /\  ch )
)  \/  ( ( ps  /\  ph )  \/  ( ps  /\  ch ) ) )  <->  ( ( ph  /\  ps )  \/  ( -.  ph  /\  ch ) ) )
292, 28bitri 249 . 2  |-  ( ( ( -.  ph  \/  ps )  /\  ( ph  \/  ch ) )  <-> 
( ( ph  /\  ps )  \/  ( -.  ph  /\  ch )
) )
301, 29bitri 249 1  |-  (if- (
ph ,  ps ,  ch )  <->  ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ch )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369  if-wif 33857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-bj-if 33858
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator