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

Theorem 3impexpbicomiVD 38115
Description: Virtual deduction proof of 3impexpbicomi 37707. 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.
 h1:: ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) qed:1,?: e0a 38020 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
3impexpbicomiVD.1 ((𝜑𝜓𝜒) → (𝜃𝜏))
Assertion
Ref Expression
3impexpbicomiVD (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃))))

Proof of Theorem 3impexpbicomiVD
StepHypRef Expression
1 3impexpbicomiVD.1 . 2 ((𝜑𝜓𝜒) → (𝜃𝜏))
2 3impexpbicom 37706 . . 3 (((𝜑𝜓𝜒) → (𝜃𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))))
32biimpi 205 . 2 (((𝜑𝜓𝜒) → (𝜃𝜏)) → (𝜑 → (𝜓 → (𝜒 → (𝜏𝜃)))))
41, 3e0a 38020 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 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator