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

Theorem imbi12VD 28922
Description: Implication form of imbi12i 317. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi12 28540 is imbi12VD 28922 without virtual deductions and was automatically derived from imbi12VD 28922.
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 28651 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ch  <->  th ) ).
2 idn1 28602 . . . . . . 7  |-  (. ( ph 
<->  ps )  ->.  ( ph  <->  ps ) ).
3 idn3 28653 . . . . . . 7  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ph  ->  ch )  ->.  ( ph  ->  ch ) ).
4 bi2 190 . . . . . . . 8  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
54imim1d 71 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ch )  ->  ( ps  ->  ch ) ) )
62, 3, 5e13 28797 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  ch ) ).
7 bi1 179 . . . . . . 7  |-  ( ( ch  <->  th )  ->  ( ch  ->  th ) )
87imim2d 50 . . . . . 6  |-  ( ( ch  <->  th )  ->  (
( ps  ->  ch )  ->  ( ps  ->  th ) ) )
91, 6, 8e23 28804 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ph  ->  ch )  ->.  ( ps  ->  th ) ).
109in3 28647 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ( ph  ->  ch )  -> 
( ps  ->  th )
) ).
11 idn3 28653 . . . . . . 7  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ps  ->  th )  ->.  ( ps  ->  th ) ).
12 bi1 179 . . . . . . . 8  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
1312imim1d 71 . . . . . . 7  |-  ( (
ph 
<->  ps )  ->  (
( ps  ->  th )  ->  ( ph  ->  th )
) )
142, 11, 13e13 28797 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  th ) ).
15 bi2 190 . . . . . . 7  |-  ( ( ch  <->  th )  ->  ( th  ->  ch ) )
1615imim2d 50 . . . . . 6  |-  ( ( ch  <->  th )  ->  (
( ph  ->  th )  ->  ( ph  ->  ch ) ) )
171, 14, 16e23 28804 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ps  ->  th )  ->.  ( ph  ->  ch ) ).
1817in3 28647 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ( ps  ->  th )  ->  ( ph  ->  ch ) ) ).
19 bi3 180 . . . 4  |-  ( ( ( ph  ->  ch )  ->  ( ps  ->  th ) )  ->  (
( ( ps  ->  th )  ->  ( ph  ->  ch ) )  -> 
( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
2010, 18, 19e22 28709 . . 3  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ).
2120in2 28643 . 2  |-  (. ( ph 
<->  ps )  ->.  ( ( ch 
<->  th )  ->  (
( ph  ->  ch )  <->  ( ps  ->  th )
) ) ).
2221in1 28599 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ph  ->  ch )  <->  ( ps  ->  th ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-vd1 28598  df-vd2 28607  df-vd3 28619
  Copyright terms: Public domain W3C validator