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 43270
Description: Virtual deduction proof of con5 42892. 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 42892 is con5VD 43270 without virtual deductions and was automatically derived from con5VD 43270.
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 42944 . . . . 5 (   (𝜑 ↔ ¬ 𝜓)   ▶   (𝜑 ↔ ¬ 𝜓)   )
2 biimpr 219 . . . . 5 ((𝜑 ↔ ¬ 𝜓) → (¬ 𝜓𝜑))
31, 2e1a 42997 . . . 4 (   (𝜑 ↔ ¬ 𝜓)   ▶   𝜓𝜑)   )
4 con3 153 . . . 4 ((¬ 𝜓𝜑) → (¬ 𝜑 → ¬ ¬ 𝜓))
53, 4e1a 42997 . . 3 (   (𝜑 ↔ ¬ 𝜓)   ▶   𝜑 → ¬ ¬ 𝜓)   )
6 notnotb 315 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
7 imbi2 349 . . . 4 ((𝜓 ↔ ¬ ¬ 𝜓) → ((¬ 𝜑𝜓) ↔ (¬ 𝜑 → ¬ ¬ 𝜓)))
87biimprcd 250 . . 3 ((¬ 𝜑 → ¬ ¬ 𝜓) → ((𝜓 ↔ ¬ ¬ 𝜓) → (¬ 𝜑𝜓)))
95, 6, 8e10 43064 . 2 (   (𝜑 ↔ ¬ 𝜓)   ▶   𝜑𝜓)   )
109in1 42941 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 42940
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator