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

Theorem orbi1rVD 39578
Description: Virtual deduction proof of orbi1r 39214. 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:: (   (𝜑𝜓)   ▶   (𝜑𝜓)   )
2:: (   (𝜑𝜓)   ,   (𝜒𝜑)    ▶   (𝜒𝜑)   )
3:2,?: e2 39354 (   (𝜑𝜓)   ,   (𝜒𝜑)    ▶   (𝜑𝜒)   )
4:1,3,?: e12 39449 (   (𝜑𝜓)   ,   (𝜒𝜑)    ▶   (𝜓𝜒)   )
5:4,?: e2 39354 (   (𝜑𝜓)   ,   (𝜒𝜑)    ▶   (𝜒𝜓)   )
6:5: (   (𝜑𝜓)   ▶   ((𝜒𝜑) → (𝜒𝜓))   )
7:: (   (𝜑𝜓)   ,   (𝜒𝜓)    ▶   (𝜒𝜓)   )
8:7,?: e2 39354 (   (𝜑𝜓)   ,   (𝜒𝜓)    ▶   (𝜓𝜒)   )
9:1,8,?: e12 39449 (   (𝜑𝜓)   ,   (𝜒𝜓)    ▶   (𝜑𝜒)   )
10:9,?: e2 39354 (   (𝜑𝜓)   ,   (𝜒𝜓)    ▶   (𝜒𝜑)   )
11:10: (   (𝜑𝜓)   ▶   ((𝜒𝜓) → (𝜒𝜑))   )
12:6,11,?: e11 39411 (   (𝜑𝜓)   ▶   ((𝜒 𝜑) ↔ (𝜒𝜓))   )
qed:12: ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
orbi1rVD ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))

Proof of Theorem orbi1rVD
StepHypRef Expression
1 idn1 39288 . . . . . 6 (   (𝜑𝜓)   ▶   (𝜑𝜓)   )
2 idn2 39336 . . . . . . 7 (   (𝜑𝜓)   ,   (𝜒𝜑)   ▶   (𝜒𝜑)   )
3 pm1.4 400 . . . . . . 7 ((𝜒𝜑) → (𝜑𝜒))
42, 3e2 39354 . . . . . 6 (   (𝜑𝜓)   ,   (𝜒𝜑)   ▶   (𝜑𝜒)   )
5 orbi1 744 . . . . . . 7 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
65biimpd 219 . . . . . 6 ((𝜑𝜓) → ((𝜑𝜒) → (𝜓𝜒)))
71, 4, 6e12 39449 . . . . 5 (   (𝜑𝜓)   ,   (𝜒𝜑)   ▶   (𝜓𝜒)   )
8 pm1.4 400 . . . . 5 ((𝜓𝜒) → (𝜒𝜓))
97, 8e2 39354 . . . 4 (   (𝜑𝜓)   ,   (𝜒𝜑)   ▶   (𝜒𝜓)   )
109in2 39328 . . 3 (   (𝜑𝜓)   ▶   ((𝜒𝜑) → (𝜒𝜓))   )
11 idn2 39336 . . . . . . 7 (   (𝜑𝜓)   ,   (𝜒𝜓)   ▶   (𝜒𝜓)   )
12 pm1.4 400 . . . . . . 7 ((𝜒𝜓) → (𝜓𝜒))
1311, 12e2 39354 . . . . . 6 (   (𝜑𝜓)   ,   (𝜒𝜓)   ▶   (𝜓𝜒)   )
145biimprd 238 . . . . . 6 ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))
151, 13, 14e12 39449 . . . . 5 (   (𝜑𝜓)   ,   (𝜒𝜓)   ▶   (𝜑𝜒)   )
16 pm1.4 400 . . . . 5 ((𝜑𝜒) → (𝜒𝜑))
1715, 16e2 39354 . . . 4 (   (𝜑𝜓)   ,   (𝜒𝜓)   ▶   (𝜒𝜑)   )
1817in2 39328 . . 3 (   (𝜑𝜓)   ▶   ((𝜒𝜓) → (𝜒𝜑))   )
19 impbi 198 . . 3 (((𝜒𝜑) → (𝜒𝜓)) → (((𝜒𝜓) → (𝜒𝜑)) → ((𝜒𝜑) ↔ (𝜒𝜓))))
2010, 18, 19e11 39411 . 2 (   (𝜑𝜓)   ▶   ((𝜒𝜑) ↔ (𝜒𝜓))   )
2120in1 39285 1 ((𝜑𝜓) → ((𝜒𝜑) ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 382
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 197  df-or 384  df-an 385  df-vd1 39284  df-vd2 39292
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator