Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifpim123g Structured version   Unicode version

Theorem ifpim123g 36114
Description: Implication of conditional logical operators. The right hand side is basically conjunctive normal form which is useful in proofs. (Contributed by RP, 16-Apr-2020.)
Assertion
Ref Expression
ifpim123g  |-  ( (if- ( ph ,  ch ,  ta )  -> if- ( ps ,  th ,  et ) )  <->  ( (
( ( ph  ->  -. 
ps )  \/  ( ch  ->  th ) )  /\  ( ( ps  ->  ph )  \/  ( ta 
->  th ) ) )  /\  ( ( (
ph  ->  ps )  \/  ( ch  ->  et ) )  /\  (
( -.  ps  ->  ph )  \/  ( ta 
->  et ) ) ) ) )

Proof of Theorem ifpim123g
StepHypRef Expression
1 dfifp4 1424 . . 3  |-  (if- (
ph ,  ch ,  ta )  <->  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) ) )
2 dfifp4 1424 . . 3  |-  (if- ( ps ,  th ,  et )  <->  ( ( -. 
ps  \/  th )  /\  ( ps  \/  et ) ) )
31, 2imbi12i 327 . 2  |-  ( (if- ( ph ,  ch ,  ta )  -> if- ( ps ,  th ,  et ) )  <->  ( (
( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  ->  ( ( -. 
ps  \/  th )  /\  ( ps  \/  et ) ) ) )
4 imor 413 . 2  |-  ( ( ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  ->  ( ( -. 
ps  \/  th )  /\  ( ps  \/  et ) ) )  <->  ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ( ( -. 
ps  \/  th )  /\  ( ps  \/  et ) ) ) )
5 ordi 872 . . 3  |-  ( ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  (
( -.  ps  \/  th )  /\  ( ps  \/  et ) ) )  <->  ( ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ( -.  ps  \/  th ) )  /\  ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ( ps  \/  et ) ) ) )
6 orass 526 . . . . 5  |-  ( ( ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  -.  ps )  \/  th )  <->  ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ( -.  ps  \/  th )
) )
7 ianor 490 . . . . . . . . . 10  |-  ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  <-> 
( -.  ( -. 
ph  \/  ch )  \/  -.  ( ph  \/  ta ) ) )
8 pm4.52 493 . . . . . . . . . . . 12  |-  ( (
ph  /\  -.  ch )  <->  -.  ( -.  ph  \/  ch ) )
98bicomi 205 . . . . . . . . . . 11  |-  ( -.  ( -.  ph  \/  ch )  <->  ( ph  /\  -.  ch ) )
10 ioran 492 . . . . . . . . . . 11  |-  ( -.  ( ph  \/  ta ) 
<->  ( -.  ph  /\  -.  ta ) )
119, 10orbi12i 523 . . . . . . . . . 10  |-  ( ( -.  ( -.  ph  \/  ch )  \/  -.  ( ph  \/  ta )
)  <->  ( ( ph  /\ 
-.  ch )  \/  ( -.  ph  /\  -.  ta ) ) )
12 cases2 980 . . . . . . . . . . 11  |-  ( ( ( ph  /\  -.  ch )  \/  ( -.  ph  /\  -.  ta ) )  <->  ( ( ph  ->  -.  ch )  /\  ( -.  ph  ->  -. 
ta ) ) )
13 imor 413 . . . . . . . . . . . 12  |-  ( (
ph  ->  -.  ch )  <->  ( -.  ph  \/  -.  ch ) )
14 pm4.66 421 . . . . . . . . . . . 12  |-  ( ( -.  ph  ->  -.  ta ) 
<->  ( ph  \/  -.  ta ) )
1513, 14anbi12i 701 . . . . . . . . . . 11  |-  ( ( ( ph  ->  -.  ch )  /\  ( -.  ph  ->  -.  ta )
)  <->  ( ( -. 
ph  \/  -.  ch )  /\  ( ph  \/  -.  ta ) ) )
1612, 15bitri 252 . . . . . . . . . 10  |-  ( ( ( ph  /\  -.  ch )  \/  ( -.  ph  /\  -.  ta ) )  <->  ( ( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta ) ) )
177, 11, 163bitri 274 . . . . . . . . 9  |-  ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  <-> 
( ( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta ) ) )
1817orbi1i 522 . . . . . . . 8  |-  ( ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  -.  ps )  <->  ( ( ( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta )
)  \/  -.  ps ) )
19 orcom 388 . . . . . . . . 9  |-  ( ( ( ( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta ) )  \/  -.  ps )  <->  ( -.  ps  \/  ( ( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta ) ) ) )
20 ordi 872 . . . . . . . . 9  |-  ( ( -.  ps  \/  (
( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta )
) )  <->  ( ( -.  ps  \/  ( -. 
ph  \/  -.  ch )
)  /\  ( -.  ps  \/  ( ph  \/  -.  ta ) ) ) )
2119, 20bitri 252 . . . . . . . 8  |-  ( ( ( ( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta ) )  \/  -.  ps )  <->  ( ( -. 
ps  \/  ( -.  ph  \/  -.  ch )
)  /\  ( -.  ps  \/  ( ph  \/  -.  ta ) ) ) )
22 orass 526 . . . . . . . . . 10  |-  ( ( ( -.  ps  \/  -.  ph )  \/  -.  ch )  <->  ( -.  ps  \/  ( -.  ph  \/  -.  ch ) ) )
23 orcom 388 . . . . . . . . . . . 12  |-  ( ( -.  ps  \/  -.  ph )  <->  ( -.  ph  \/  -.  ps ) )
24 imor 413 . . . . . . . . . . . 12  |-  ( (
ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) )
2523, 24bitr4i 255 . . . . . . . . . . 11  |-  ( ( -.  ps  \/  -.  ph )  <->  ( ph  ->  -. 
ps ) )
2625orbi1i 522 . . . . . . . . . 10  |-  ( ( ( -.  ps  \/  -.  ph )  \/  -.  ch )  <->  ( ( ph  ->  -.  ps )  \/ 
-.  ch ) )
2722, 26bitr3i 254 . . . . . . . . 9  |-  ( ( -.  ps  \/  ( -.  ph  \/  -.  ch ) )  <->  ( ( ph  ->  -.  ps )  \/  -.  ch ) )
28 orass 526 . . . . . . . . . 10  |-  ( ( ( -.  ps  \/  ph )  \/  -.  ta ) 
<->  ( -.  ps  \/  ( ph  \/  -.  ta ) ) )
29 imor 413 . . . . . . . . . . . 12  |-  ( ( ps  ->  ph )  <->  ( -.  ps  \/  ph ) )
3029bicomi 205 . . . . . . . . . . 11  |-  ( ( -.  ps  \/  ph ) 
<->  ( ps  ->  ph )
)
3130orbi1i 522 . . . . . . . . . 10  |-  ( ( ( -.  ps  \/  ph )  \/  -.  ta ) 
<->  ( ( ps  ->  ph )  \/  -.  ta ) )
3228, 31bitr3i 254 . . . . . . . . 9  |-  ( ( -.  ps  \/  ( ph  \/  -.  ta )
)  <->  ( ( ps 
->  ph )  \/  -.  ta ) )
3327, 32anbi12i 701 . . . . . . . 8  |-  ( ( ( -.  ps  \/  ( -.  ph  \/  -.  ch ) )  /\  ( -.  ps  \/  ( ph  \/  -.  ta ) ) )  <->  ( ( (
ph  ->  -.  ps )  \/  -.  ch )  /\  ( ( ps  ->  ph )  \/  -.  ta ) ) )
3418, 21, 333bitri 274 . . . . . . 7  |-  ( ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  -.  ps )  <->  ( ( (
ph  ->  -.  ps )  \/  -.  ch )  /\  ( ( ps  ->  ph )  \/  -.  ta ) ) )
3534orbi1i 522 . . . . . 6  |-  ( ( ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  -.  ps )  \/  th )  <->  ( ( ( ( ph  ->  -.  ps )  \/ 
-.  ch )  /\  (
( ps  ->  ph )  \/  -.  ta ) )  \/  th ) )
36 ordir 873 . . . . . 6  |-  ( ( ( ( ( ph  ->  -.  ps )  \/ 
-.  ch )  /\  (
( ps  ->  ph )  \/  -.  ta ) )  \/  th )  <->  ( (
( ( ph  ->  -. 
ps )  \/  -.  ch )  \/  th )  /\  ( ( ( ps 
->  ph )  \/  -.  ta )  \/  th )
) )
37 orass 526 . . . . . . . 8  |-  ( ( ( ( ph  ->  -. 
ps )  \/  -.  ch )  \/  th )  <->  ( ( ph  ->  -.  ps )  \/  ( -.  ch  \/  th )
) )
38 imor 413 . . . . . . . . . 10  |-  ( ( ch  ->  th )  <->  ( -.  ch  \/  th ) )
3938bicomi 205 . . . . . . . . 9  |-  ( ( -.  ch  \/  th ) 
<->  ( ch  ->  th )
)
4039orbi2i 521 . . . . . . . 8  |-  ( ( ( ph  ->  -.  ps )  \/  ( -.  ch  \/  th )
)  <->  ( ( ph  ->  -.  ps )  \/  ( ch  ->  th )
) )
4137, 40bitri 252 . . . . . . 7  |-  ( ( ( ( ph  ->  -. 
ps )  \/  -.  ch )  \/  th )  <->  ( ( ph  ->  -.  ps )  \/  ( ch  ->  th ) ) )
42 orass 526 . . . . . . . 8  |-  ( ( ( ( ps  ->  ph )  \/  -.  ta )  \/  th )  <->  ( ( ps  ->  ph )  \/  ( -.  ta  \/  th ) ) )
43 imor 413 . . . . . . . . . 10  |-  ( ( ta  ->  th )  <->  ( -.  ta  \/  th ) )
4443bicomi 205 . . . . . . . . 9  |-  ( ( -.  ta  \/  th ) 
<->  ( ta  ->  th )
)
4544orbi2i 521 . . . . . . . 8  |-  ( ( ( ps  ->  ph )  \/  ( -.  ta  \/  th ) )  <->  ( ( ps  ->  ph )  \/  ( ta  ->  th ) ) )
4642, 45bitri 252 . . . . . . 7  |-  ( ( ( ( ps  ->  ph )  \/  -.  ta )  \/  th )  <->  ( ( ps  ->  ph )  \/  ( ta  ->  th )
) )
4741, 46anbi12i 701 . . . . . 6  |-  ( ( ( ( ( ph  ->  -.  ps )  \/ 
-.  ch )  \/  th )  /\  ( ( ( ps  ->  ph )  \/ 
-.  ta )  \/  th ) )  <->  ( (
( ph  ->  -.  ps )  \/  ( ch  ->  th ) )  /\  ( ( ps  ->  ph )  \/  ( ta 
->  th ) ) ) )
4835, 36, 473bitri 274 . . . . 5  |-  ( ( ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  -.  ps )  \/  th )  <->  ( ( ( ph  ->  -. 
ps )  \/  ( ch  ->  th ) )  /\  ( ( ps  ->  ph )  \/  ( ta 
->  th ) ) ) )
496, 48bitr3i 254 . . . 4  |-  ( ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ( -.  ps  \/  th )
)  <->  ( ( (
ph  ->  -.  ps )  \/  ( ch  ->  th )
)  /\  ( ( ps  ->  ph )  \/  ( ta  ->  th ) ) ) )
50 orass 526 . . . . 5  |-  ( ( ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ps )  \/  et )  <->  ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ( ps  \/  et ) ) )
5117orbi1i 522 . . . . . . . 8  |-  ( ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ps ) 
<->  ( ( ( -. 
ph  \/  -.  ch )  /\  ( ph  \/  -.  ta ) )  \/  ps ) )
52 orcom 388 . . . . . . . . 9  |-  ( ( ( ( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta ) )  \/  ps ) 
<->  ( ps  \/  (
( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta )
) ) )
53 ordi 872 . . . . . . . . 9  |-  ( ( ps  \/  ( ( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta )
) )  <->  ( ( ps  \/  ( -.  ph  \/  -.  ch ) )  /\  ( ps  \/  ( ph  \/  -.  ta ) ) ) )
5452, 53bitri 252 . . . . . . . 8  |-  ( ( ( ( -.  ph  \/  -.  ch )  /\  ( ph  \/  -.  ta ) )  \/  ps ) 
<->  ( ( ps  \/  ( -.  ph  \/  -.  ch ) )  /\  ( ps  \/  ( ph  \/  -.  ta ) ) ) )
55 orass 526 . . . . . . . . . 10  |-  ( ( ( ps  \/  -.  ph )  \/  -.  ch ) 
<->  ( ps  \/  ( -.  ph  \/  -.  ch ) ) )
56 orcom 388 . . . . . . . . . . . 12  |-  ( ( ps  \/  -.  ph ) 
<->  ( -.  ph  \/  ps ) )
57 imor 413 . . . . . . . . . . . 12  |-  ( (
ph  ->  ps )  <->  ( -.  ph  \/  ps ) )
5856, 57bitr4i 255 . . . . . . . . . . 11  |-  ( ( ps  \/  -.  ph ) 
<->  ( ph  ->  ps ) )
5958orbi1i 522 . . . . . . . . . 10  |-  ( ( ( ps  \/  -.  ph )  \/  -.  ch ) 
<->  ( ( ph  ->  ps )  \/  -.  ch ) )
6055, 59bitr3i 254 . . . . . . . . 9  |-  ( ( ps  \/  ( -. 
ph  \/  -.  ch )
)  <->  ( ( ph  ->  ps )  \/  -.  ch ) )
61 orass 526 . . . . . . . . . 10  |-  ( ( ( ps  \/  ph )  \/  -.  ta )  <->  ( ps  \/  ( ph  \/  -.  ta ) ) )
62 df-or 371 . . . . . . . . . . 11  |-  ( ( ps  \/  ph )  <->  ( -.  ps  ->  ph )
)
6362orbi1i 522 . . . . . . . . . 10  |-  ( ( ( ps  \/  ph )  \/  -.  ta )  <->  ( ( -.  ps  ->  ph )  \/  -.  ta ) )
6461, 63bitr3i 254 . . . . . . . . 9  |-  ( ( ps  \/  ( ph  \/  -.  ta ) )  <-> 
( ( -.  ps  ->  ph )  \/  -.  ta ) )
6560, 64anbi12i 701 . . . . . . . 8  |-  ( ( ( ps  \/  ( -.  ph  \/  -.  ch ) )  /\  ( ps  \/  ( ph  \/  -.  ta ) ) )  <-> 
( ( ( ph  ->  ps )  \/  -.  ch )  /\  (
( -.  ps  ->  ph )  \/  -.  ta ) ) )
6651, 54, 653bitri 274 . . . . . . 7  |-  ( ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ps ) 
<->  ( ( ( ph  ->  ps )  \/  -.  ch )  /\  (
( -.  ps  ->  ph )  \/  -.  ta ) ) )
6766orbi1i 522 . . . . . 6  |-  ( ( ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ps )  \/  et )  <->  ( ( ( ( ph  ->  ps )  \/  -.  ch )  /\  (
( -.  ps  ->  ph )  \/  -.  ta ) )  \/  et ) )
68 ordir 873 . . . . . 6  |-  ( ( ( ( ( ph  ->  ps )  \/  -.  ch )  /\  (
( -.  ps  ->  ph )  \/  -.  ta ) )  \/  et ) 
<->  ( ( ( (
ph  ->  ps )  \/ 
-.  ch )  \/  et )  /\  ( ( ( -.  ps  ->  ph )  \/  -.  ta )  \/  et ) ) )
69 orass 526 . . . . . . . 8  |-  ( ( ( ( ph  ->  ps )  \/  -.  ch )  \/  et )  <->  ( ( ph  ->  ps )  \/  ( -.  ch  \/  et ) ) )
70 imor 413 . . . . . . . . . 10  |-  ( ( ch  ->  et )  <->  ( -.  ch  \/  et ) )
7170bicomi 205 . . . . . . . . 9  |-  ( ( -.  ch  \/  et ) 
<->  ( ch  ->  et ) )
7271orbi2i 521 . . . . . . . 8  |-  ( ( ( ph  ->  ps )  \/  ( -.  ch  \/  et ) )  <-> 
( ( ph  ->  ps )  \/  ( ch 
->  et ) ) )
7369, 72bitri 252 . . . . . . 7  |-  ( ( ( ( ph  ->  ps )  \/  -.  ch )  \/  et )  <->  ( ( ph  ->  ps )  \/  ( ch  ->  et ) ) )
74 orass 526 . . . . . . . 8  |-  ( ( ( ( -.  ps  ->  ph )  \/  -.  ta )  \/  et ) 
<->  ( ( -.  ps  ->  ph )  \/  ( -.  ta  \/  et ) ) )
75 imor 413 . . . . . . . . . 10  |-  ( ( ta  ->  et )  <->  ( -.  ta  \/  et ) )
7675bicomi 205 . . . . . . . . 9  |-  ( ( -.  ta  \/  et ) 
<->  ( ta  ->  et ) )
7776orbi2i 521 . . . . . . . 8  |-  ( ( ( -.  ps  ->  ph )  \/  ( -. 
ta  \/  et )
)  <->  ( ( -. 
ps  ->  ph )  \/  ( ta  ->  et ) ) )
7874, 77bitri 252 . . . . . . 7  |-  ( ( ( ( -.  ps  ->  ph )  \/  -.  ta )  \/  et ) 
<->  ( ( -.  ps  ->  ph )  \/  ( ta  ->  et ) ) )
7973, 78anbi12i 701 . . . . . 6  |-  ( ( ( ( ( ph  ->  ps )  \/  -.  ch )  \/  et )  /\  ( ( ( -.  ps  ->  ph )  \/  -.  ta )  \/  et ) )  <->  ( (
( ph  ->  ps )  \/  ( ch  ->  et ) )  /\  (
( -.  ps  ->  ph )  \/  ( ta 
->  et ) ) ) )
8067, 68, 793bitri 274 . . . . 5  |-  ( ( ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ps )  \/  et )  <->  ( ( ( ph  ->  ps )  \/  ( ch 
->  et ) )  /\  ( ( -.  ps  ->  ph )  \/  ( ta  ->  et ) ) ) )
8150, 80bitr3i 254 . . . 4  |-  ( ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ( ps  \/  et ) )  <-> 
( ( ( ph  ->  ps )  \/  ( ch  ->  et ) )  /\  ( ( -. 
ps  ->  ph )  \/  ( ta  ->  et ) ) ) )
8249, 81anbi12i 701 . . 3  |-  ( ( ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ( -.  ps  \/  th )
)  /\  ( -.  ( ( -.  ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  ( ps  \/  et ) ) )  <->  ( (
( ( ph  ->  -. 
ps )  \/  ( ch  ->  th ) )  /\  ( ( ps  ->  ph )  \/  ( ta 
->  th ) ) )  /\  ( ( (
ph  ->  ps )  \/  ( ch  ->  et ) )  /\  (
( -.  ps  ->  ph )  \/  ( ta 
->  et ) ) ) ) )
835, 82bitri 252 . 2  |-  ( ( -.  ( ( -. 
ph  \/  ch )  /\  ( ph  \/  ta ) )  \/  (
( -.  ps  \/  th )  /\  ( ps  \/  et ) ) )  <->  ( ( ( ( ph  ->  -.  ps )  \/  ( ch  ->  th ) )  /\  ( ( ps  ->  ph )  \/  ( ta 
->  th ) ) )  /\  ( ( (
ph  ->  ps )  \/  ( ch  ->  et ) )  /\  (
( -.  ps  ->  ph )  \/  ( ta 
->  et ) ) ) ) )
843, 4, 833bitri 274 1  |-  ( (if- ( ph ,  ch ,  ta )  -> if- ( ps ,  th ,  et ) )  <->  ( (
( ( ph  ->  -. 
ps )  \/  ( ch  ->  th ) )  /\  ( ( ps  ->  ph )  \/  ( ta 
->  th ) ) )  /\  ( ( (
ph  ->  ps )  \/  ( ch  ->  et ) )  /\  (
( -.  ps  ->  ph )  \/  ( ta 
->  et ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370  if-wif 1420
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 188  df-or 371  df-an 372  df-ifp 1421
This theorem is referenced by:  ifpim1g  36115  ifpbi1b  36117  ifpimimb  36118  ifpor123g  36122  ifpimim  36123
  Copyright terms: Public domain W3C validator