Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  imbi12VD Structured version   Unicode version

Theorem imbi12VD 33774
Description: Implication form of imbi12i 326. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi12 322 is imbi12VD 33774 without virtual deductions and was automatically derived from imbi12VD 33774.
1::  |-  (. ( ph  <->  ps )  ->.  ( ph  <->  ps ) ).
2::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ch  <->  th ) ).
3::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ph  ->  ch )  ->.  ( ph  ->  ch ) ).
4:1,3:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  ch ) ).
5:2,4:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  th ) ).
6:5:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ph  ->  ch )  ->  ( ps  ->  th ) ) ).
7::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ps  ->  th )  ->.  ( ps  ->  th ) ).
8:1,7:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  th ) ).
9:2,8:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  ch ) ).
10:9:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ps  ->  th )  ->  ( ph  ->  ch ) ) ).
11:6,10:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ).
12:11:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) ).
qed:12:  |-  ( ( ph  <->  ps )  ->  ( ( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
imbi12VD  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )

Proof of Theorem imbi12VD
StepHypRef Expression
1 idn2 33500 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ch  <->  th ) ).
2 idn1 33452 . . . . . . 7  |-  (. ( ph 
<->  ps )  ->.  ( ph  <->  ps ) ).
3 idn3 33502 . . . . . . 7  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ph  ->  ch )  ->.  ( ph  ->  ch ) ).
4 bi2 198 . . . . . . . 8  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
54imim1d 75 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ch )  ->  ( ps  ->  ch ) ) )
62, 3, 5e13 33646 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  ch ) ).
7 bi1 186 . . . . . . 7  |-  ( ( ch  <->  th )  ->  ( ch  ->  th ) )
87imim2d 52 . . . . . 6  |-  ( ( ch  <->  th )  ->  (
( ps  ->  ch )  ->  ( ps  ->  th ) ) )
91, 6, 8e23 33653 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  th ) ).
109in3 33496 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ( ph  ->  ch )  -> 
( ps  ->  th )
) ).
11 idn3 33502 . . . . . . 7  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ps  ->  th )  ->.  ( ps  ->  th ) ).
12 bi1 186 . . . . . . . 8  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
1312imim1d 75 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  (
( ps  ->  th )  ->  ( ph  ->  th )
) )
142, 11, 13e13 33646 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  th ) ).
15 bi2 198 . . . . . . 7  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
1615imim2d 52 . . . . . 6  |-  ( ( ch  <->  th )  ->  (
( ph  ->  th )  ->  ( ph  ->  ch ) ) )
171, 14, 16e23 33653 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  ch ) ).
1817in3 33496 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ( ps  ->  th )  ->  ( ph  ->  ch ) ) ).
19 bi3 187 . . . 4  |-  ( ( ( ph  ->  ch )  ->  ( ps  ->  th ) )  ->  (
( ( ps  ->  th )  ->  ( ph  ->  ch ) )  -> 
( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
2010, 18, 19e22 33558 . . 3  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ).
2120in2 33492 . 2  |-  (. ( ph 
<->  ps )  ->.  ( ( ch 
<->  th )  ->  (
( ph  ->  ch )  <->  ( ps  ->  th )
) ) ).
2221in1 33449 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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-an 371  df-3an 975  df-vd1 33448  df-vd2 33456  df-vd3 33468
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator