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

Theorem 3impexpbicomVD 28633
Description: Virtual deduction proof of 3impexpbicom 1357. 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 28467  |-  (. ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
4:3,?: e1_ 28399  |-  (. ( ( 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,?: e1_ 28399  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) ) ).
8:7,2,?: e10 28467  |-  (. ( 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 28543  |-  ( ( ( 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 28342 . . . . 5  |-  (. (
( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta )
) ).
2 bicom 191 . . . . 5  |-  ( ( th  <->  ta )  <->  ( ta  <->  th ) )
3 imbi2 314 . . . . . 6  |-  ( ( ( th  <->  ta )  <->  ( ta  <->  th ) )  -> 
( ( ( ph  /\ 
ps  /\  ch )  ->  ( th  <->  ta )
)  <->  ( ( ph  /\ 
ps  /\  ch )  ->  ( ta  <->  th )
) ) )
43biimpcd 215 . . . . 5  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( th 
<->  ta ) )  -> 
( ( ( th  <->  ta )  <->  ( ta  <->  th )
)  ->  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th )
) ) )
51, 2, 4e10 28467 . . . 4  |-  (. (
( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th )
) ).
6 3impexp 1356 . . . . 5  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( ta 
<->  th ) )  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) )
76biimpi 186 . . . 4  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( ta 
<->  th ) )  -> 
( ph  ->  ( ps 
->  ( ch  ->  ( ta 
<->  th ) ) ) ) )
85, 7e1_ 28399 . . 3  |-  (. (
( ph  /\  ps  /\  ch )  ->  ( th  <->  ta ) )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) ).
98in1 28339 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( th 
<->  ta ) )  -> 
( ph  ->  ( ps 
->  ( ch  ->  ( ta 
<->  th ) ) ) ) )
10 idn1 28342 . . . . 5  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ph  ->  ( ps  ->  ( ch  ->  ( ta 
<->  th ) ) ) ) ).
116biimpri 197 . . . . 5  |-  ( (
ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->  ( ( ph  /\ 
ps  /\  ch )  ->  ( ta  <->  th )
) )
1210, 11e1_ 28399 . . . 4  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  -> 
( ta  <->  th )
) ).
133biimprcd 216 . . . 4  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( ta 
<->  th ) )  -> 
( ( ( th  <->  ta )  <->  ( ta  <->  th )
)  ->  ( ( ph  /\  ps  /\  ch )  ->  ( th  <->  ta )
) ) )
1412, 2, 13e10 28467 . . 3  |-  (. ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->.  ( ( ph  /\  ps  /\  ch )  -> 
( th  <->  ta )
) ).
1514in1 28339 . 2  |-  ( (
ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th ) ) ) )  ->  ( ( ph  /\ 
ps  /\  ch )  ->  ( th  <->  ta )
) )
16 bi3 179 . 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 28543 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  ->  ( th 
<->  ta ) )  <->  ( ph  ->  ( ps  ->  ( ch  ->  ( ta  <->  th )
) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934
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 177  df-an 360  df-3an 936  df-vd1 28338
  Copyright terms: Public domain W3C validator