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

Theorem 3impexpbicomVD 33390
Description: Virtual deduction proof of 3impexpbicom 32954. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1::  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) ) ).
2::  |-  ( ( th  <->  ta )  <->  ( ta  <->  th ) )
3:1,2,?: e10 33213  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
4:3,?: e1a 33146  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) ) ).
5:4:  |-  ( ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) ) )
6::  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) ) ).
7:6,?: e1a 33146  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
8:7,2,?: e10 33213  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) ) ).
9:8:  |-  ( ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) ) )
qed:5,9,?: e00 33298  |-  ( ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) ) )
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
3impexpbicomVD  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( th 
<->  ta ) )  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) )

Proof of Theorem 3impexpbicomVD
StepHypRef Expression
1 idn1 33084 . . . . 5  |-  (. (
( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta )
) ).
2 bicom 200 . . . . 5  |-  ( ( th  <->  ta )  <->  ( ta  <->  th ) )
3 imbi2 324 . . . . . 6  |-  ( ( ( th  <->  ta )  <->  ( ta  <->  th ) )  -> 
( ( ( ph  /\ 
ps  /\  ch )  ->  ( th  <->  ta )
)  <->  ( ( ph  /\ 
ps  /\  ch )  ->  ( ta  <->  th )
) ) )
43biimpcd 224 . . . . 5  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( th 
<->  ta ) )  -> 
( ( ( th  <->  ta )  <->  ( ta  <->  th )
)  ->  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th )
) ) )
51, 2, 4e10 33213 . . . 4  |-  (. (
( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th )
) ).
6 3impexp 32953 . . . . 5  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( ta 
<->  th ) )  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) )
76biimpi 194 . . . 4  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( ta 
<->  th ) )  -> 
( ph  ->  ( ps 
->  ( ch  ->  ( ta 
<->  th ) ) ) ) )
85, 7e1a 33146 . . 3  |-  (. (
( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) ).
98in1 33081 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( th 
<->  ta ) )  -> 
( ph  ->  ( ps 
->  ( ch  ->  ( ta 
<->  th ) ) ) ) )
10 idn1 33084 . . . . 5  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  ( ta 
<->  th ) ) ) ) ).
116biimpri 206 . . . . 5  |-  ( (
ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->  ( ( ph  /\ 
ps  /\  ch )  ->  ( ta  <->  th )
) )
1210, 11e1a 33146 . . . 4  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  -> 
( ta  <->  th )
) ).
133biimprcd 225 . . . 4  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( ta 
<->  th ) )  -> 
( ( ( th  <->  ta )  <->  ( ta  <->  th )
)  ->  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta )
) ) )
1412, 2, 13e10 33213 . . 3  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  -> 
( th  <->  ta )
) ).
1514in1 33081 . 2  |-  ( (
ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->  ( ( ph  /\ 
ps  /\  ch )  ->  ( th  <->  ta )
) )
16 bi3 187 . 2  |-  ( ( ( ( ph  /\  ps  /\  ch )  -> 
( th  <->  ta )
)  ->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) )  ->  ( ( (
ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->  ( ( ph  /\ 
ps  /\  ch )  ->  ( th  <->  ta )
) )  ->  (
( ( ph  /\  ps  /\  ch )  -> 
( th  <->  ta )
)  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) ) ) )
179, 15, 16e00 33298 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( th 
<->  ta ) )  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 974
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 976  df-vd1 33080
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator