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

Theorem con5VD 44339
Description: Virtual deduction proof of con5 43961. 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. con5 43961 is con5VD 44339 without virtual deductions and was automatically derived from con5VD 44339.
1:: (   (𝜑 ↔ ¬ 𝜓)   ▶   (𝜑 ↔ ¬ 𝜓)   )
2:1: (   (𝜑 ↔ ¬ 𝜓)   ▶   𝜓𝜑)   )
3:2: (   (𝜑 ↔ ¬ 𝜓)   ▶   𝜑 → ¬ ¬ 𝜓 )   )
4:: (𝜓 ↔ ¬ ¬ 𝜓)
5:3,4: (   (𝜑 ↔ ¬ 𝜓)   ▶   𝜑𝜓)   )
qed:5: ((𝜑 ↔ ¬ 𝜓) → (¬ 𝜑𝜓))
(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
con5VD ((𝜑 ↔ ¬ 𝜓) → (¬ 𝜑𝜓))

Proof of Theorem con5VD
StepHypRef Expression
1 idn1 44013 . . . . 5 (   (𝜑 ↔ ¬ 𝜓)   ▶   (𝜑 ↔ ¬ 𝜓)   )
2 biimpr 219 . . . . 5 ((𝜑 ↔ ¬ 𝜓) → (¬ 𝜓𝜑))
31, 2e1a 44066 . . . 4 (   (𝜑 ↔ ¬ 𝜓)   ▶   𝜓𝜑)   )
4 con3 153 . . . 4 ((¬ 𝜓𝜑) → (¬ 𝜑 → ¬ ¬ 𝜓))
53, 4e1a 44066 . . 3 (   (𝜑 ↔ ¬ 𝜓)   ▶   𝜑 → ¬ ¬ 𝜓)   )
6 notnotb 315 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
7 imbi2 348 . . . 4 ((𝜓 ↔ ¬ ¬ 𝜓) → ((¬ 𝜑𝜓) ↔ (¬ 𝜑 → ¬ ¬ 𝜓)))
87biimprcd 249 . . 3 ((¬ 𝜑 → ¬ ¬ 𝜓) → ((𝜓 ↔ ¬ ¬ 𝜓) → (¬ 𝜑𝜓)))
95, 6, 8e10 44133 . 2 (   (𝜑 ↔ ¬ 𝜓)   ▶   𝜑𝜓)   )
109in1 44010 1 ((𝜑 ↔ ¬ 𝜓) → (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205
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 206  df-vd1 44009
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator