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

Theorem imbi13VD 28988
Description: Join three logical equivalences to form equivalence of implications. 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. imbi13 28606 is imbi13VD 28988 without virtual deductions and was automatically derived from imbi13VD 28988.
1::  |-  (. ( ph  <->  ps )  ->.  ( ph  <->  ps ) ).
2::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ch  <->  th ) ).
3::  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ta  <->  et )  ->.  ( ta  <->  et ) ).
4:2,3:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ta  <->  et )  ->.  ( ( ch  ->  ta )  <->  ( th  ->  et ) ) ).
5:1,4:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th ) ,. ( ta  <->  et )  ->.  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ).
6:5:  |-  (. ( ph  <->  ps ) ,. ( ch  <->  th )  ->.  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ).
7:6:  |-  (. ( ph  <->  ps )  ->.  ( ( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ) ).
qed:7:  |-  ( ( ph  <->  ps )  ->  ( ( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ) )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
imbi13VD  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta )
)  <->  ( ps  ->  ( th  ->  et )
) ) ) ) )

Proof of Theorem imbi13VD
StepHypRef Expression
1 idn1 28667 . . . . 5  |-  (. ( ph 
<->  ps )  ->.  ( ph  <->  ps ) ).
2 idn2 28716 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ch  <->  th ) ).
3 idn3 28718 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ta 
<->  et )  ->.  ( ta  <->  et ) ).
4 imbi12 28605 . . . . . 6  |-  ( ( ch  <->  th )  ->  (
( ta  <->  et )  ->  ( ( ch  ->  ta )  <->  ( th  ->  et ) ) ) )
52, 3, 4e23 28869 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ta 
<->  et )  ->.  ( ( ch  ->  ta )  <->  ( th  ->  et ) ) ).
6 imbi12 28605 . . . . 5  |-  ( (
ph 
<->  ps )  ->  (
( ( ch  ->  ta )  <->  ( th  ->  et ) )  ->  (
( ph  ->  ( ch 
->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) )
71, 5, 6e13 28862 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ta 
<->  et )  ->.  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ).
87in3 28712 . . 3  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ( ta 
<->  et )  ->  (
( ph  ->  ( ch 
->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ).
98in2 28708 . 2  |-  (. ( ph 
<->  ps )  ->.  ( ( ch 
<->  th )  ->  (
( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta )
)  <->  ( ps  ->  ( th  ->  et )
) ) ) ) ).
109in1 28664 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta )
)  <->  ( ps  ->  ( th  ->  et )
) ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
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 179  df-an 362  df-3an 939  df-vd1 28663  df-vd2 28672  df-vd3 28684
  Copyright terms: Public domain W3C validator