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

Theorem exbiriVD 38111
Description: Virtual deduction proof of exbiri 650. 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:: ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) 2:: ⊢ (   𝜑   ▶   𝜑   ) 3:: ⊢ (   𝜑   ,   𝜓   ▶   𝜓   ) 4:: ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   ) 5:2,1,?: e10 37940 ⊢ (   𝜑   ▶   (𝜓 → (𝜒 ↔ 𝜃))   ) 6:3,5,?: e21 37978 ⊢ (   𝜑   ,   𝜓   ▶   (𝜒 ↔ 𝜃)   ) 7:4,6,?: e32 38006 ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   ) 8:7: ⊢ (   𝜑   ,   𝜓   ▶   (𝜃 → 𝜒)   ) 9:8: ⊢ (   𝜑   ▶   (𝜓 → (𝜃 → 𝜒))   ) qed:9: ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
exbiriVD.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
exbiriVD (𝜑 → (𝜓 → (𝜃𝜒)))

Proof of Theorem exbiriVD
StepHypRef Expression
1 idn3 37861 . . . . 5 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2 idn2 37859 . . . . . 6 (   𝜑   ,   𝜓   ▶   𝜓   )
3 idn1 37811 . . . . . . 7 (   𝜑   ▶   𝜑   )
4 exbiriVD.1 . . . . . . 7 ((𝜑𝜓) → (𝜒𝜃))
5 pm3.3 459 . . . . . . . 8 (((𝜑𝜓) → (𝜒𝜃)) → (𝜑 → (𝜓 → (𝜒𝜃))))
65com12 32 . . . . . . 7 (𝜑 → (((𝜑𝜓) → (𝜒𝜃)) → (𝜓 → (𝜒𝜃))))
73, 4, 6e10 37940 . . . . . 6 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
8 pm2.27 41 . . . . . 6 (𝜓 → ((𝜓 → (𝜒𝜃)) → (𝜒𝜃)))
92, 7, 8e21 37978 . . . . 5 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
10 biimpr 209 . . . . . 6 ((𝜒𝜃) → (𝜃𝜒))
1110com12 32 . . . . 5 (𝜃 → ((𝜒𝜃) → 𝜒))
121, 9, 11e32 38006 . . . 4 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
1312in3 37855 . . 3 (   𝜑   ,   𝜓   ▶   (𝜃𝜒)   )
1413in2 37851 . 2 (   𝜑   ▶   (𝜓 → (𝜃𝜒))   )
1514in1 37808 1 (𝜑 → (𝜓 → (𝜃𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383 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  df-vd2 37815  df-vd3 37827 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator