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

Theorem imbi13VD 33775
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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi13 33391 is imbi13VD 33775 without virtual deductions and was automatically derived from imbi13VD 33775.
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 33452 . . . . 5  |-  (. ( ph 
<->  ps )  ->.  ( ph  <->  ps ) ).
2 idn2 33500 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ch  <->  th ) ).
3 idn3 33502 . . . . . 6  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ta 
<->  et )  ->.  ( ta  <->  et ) ).
4 imbi12 322 . . . . . 6  |-  ( ( ch  <->  th )  ->  (
( ta  <->  et )  ->  ( ( ch  ->  ta )  <->  ( th  ->  et ) ) ) )
52, 3, 4e23 33653 . . . . 5  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ta 
<->  et )  ->.  ( ( ch  ->  ta )  <->  ( th  ->  et ) ) ).
6 imbi12 322 . . . . 5  |-  ( (
ph 
<->  ps )  ->  (
( ( ch  ->  ta )  <->  ( th  ->  et ) )  ->  (
( ph  ->  ( ch 
->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) )
71, 5, 6e13 33646 . . . 4  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th ) ,. ( ta 
<->  et )  ->.  ( ( ph  ->  ( ch  ->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ).
87in3 33496 . . 3  |-  (. ( ph 
<->  ps ) ,. ( ch 
<->  th )  ->.  ( ( ta 
<->  et )  ->  (
( ph  ->  ( ch 
->  ta ) )  <->  ( ps  ->  ( th  ->  et ) ) ) ) ).
98in2 33492 . 2  |-  (. ( ph 
<->  ps )  ->.  ( ( ch 
<->  th )  ->  (
( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta )
)  <->  ( ps  ->  ( th  ->  et )
) ) ) ) ).
109in1 33449 1  |-  ( (
ph 
<->  ps )  ->  (
( ch  <->  th )  ->  ( ( ta  <->  et )  ->  ( ( ph  ->  ( ch  ->  ta )
)  <->  ( ps  ->  ( th  ->  et )
) ) ) ) )
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