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

Theorem 3impexpbicomVD 38114
Description: Virtual deduction proof of 3impexpbicom 37706. 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:1,2,?: e10 37940 (   ((𝜑𝜓𝜒) → (𝜃𝜏))   ▶   ((𝜑𝜓𝜒) → (𝜏𝜃))   )
4:3,?: e1a 37873 (   ((𝜑𝜓𝜒) → (𝜃𝜏))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 𝜃))))   )
5:4: (((𝜑𝜓𝜒) → (𝜃𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏 𝜃)))))
6:: (   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏 𝜃))))   )
7:6,?: e1a 37873 (   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   ▶   ((𝜑𝜓𝜒) → (𝜏 𝜃))   )
8:7,2,?: e10 37940 (   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   ▶   ((𝜑𝜓𝜒) → (𝜃 𝜏))   )
9:8: ((𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))) → ((𝜑𝜓𝜒) → (𝜃 𝜏)))
qed:5,9,?: e00 38016 (((𝜑𝜓𝜒) → (𝜃𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 𝜃)))))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
3impexpbicomVD (((𝜑𝜓𝜒) → (𝜃𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))))

Proof of Theorem 3impexpbicomVD
StepHypRef Expression
1 idn1 37811 . . . . 5 (   ((𝜑𝜓𝜒) → (𝜃𝜏))   ▶   ((𝜑𝜓𝜒) → (𝜃𝜏))   )
2 bicom 211 . . . . 5 ((𝜃𝜏) ↔ (𝜏𝜃))
3 imbi2 337 . . . . . 6 (((𝜃𝜏) ↔ (𝜏𝜃)) → (((𝜑𝜓𝜒) → (𝜃𝜏)) ↔ ((𝜑𝜓𝜒) → (𝜏𝜃))))
43biimpcd 238 . . . . 5 (((𝜑𝜓𝜒) → (𝜃𝜏)) → (((𝜃𝜏) ↔ (𝜏𝜃)) → ((𝜑𝜓𝜒) → (𝜏𝜃))))
51, 2, 4e10 37940 . . . 4 (   ((𝜑𝜓𝜒) → (𝜃𝜏))   ▶   ((𝜑𝜓𝜒) → (𝜏𝜃))   )
6 3impexp 1281 . . . . 5 (((𝜑𝜓𝜒) → (𝜏𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))))
76biimpi 205 . . . 4 (((𝜑𝜓𝜒) → (𝜏𝜃)) → (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))))
85, 7e1a 37873 . . 3 (   ((𝜑𝜓𝜒) → (𝜃𝜏))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   )
98in1 37808 . 2 (((𝜑𝜓𝜒) → (𝜃𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))))
10 idn1 37811 . . . . 5 (   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   ▶   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   )
116biimpri 217 . . . . 5 ((𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))) → ((𝜑𝜓𝜒) → (𝜏𝜃)))
1210, 11e1a 37873 . . . 4 (   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   ▶   ((𝜑𝜓𝜒) → (𝜏𝜃))   )
133biimprcd 239 . . . 4 (((𝜑𝜓𝜒) → (𝜏𝜃)) → (((𝜃𝜏) ↔ (𝜏𝜃)) → ((𝜑𝜓𝜒) → (𝜃𝜏))))
1412, 2, 13e10 37940 . . 3 (   (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))   ▶   ((𝜑𝜓𝜒) → (𝜃𝜏))   )
1514in1 37808 . 2 ((𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))) → ((𝜑𝜓𝜒) → (𝜃𝜏)))
16 impbi 197 . 2 ((((𝜑𝜓𝜒) → (𝜃𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))) → (((𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))) → ((𝜑𝜓𝜒) → (𝜃𝜏))) → (((𝜑𝜓𝜒) → (𝜃𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))))))
179, 15, 16e00 38016 1 (((𝜑𝜓𝜒) → (𝜃𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  w3a 1031
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 196  df-an 385  df-3an 1033  df-vd1 37807
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator