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

Theorem exbiriVD 39846
Description: Virtual deduction proof of exbiri 846. 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 39685 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
6:3,5,?: e21 39722 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
7:4,6,?: e32 39750 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
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 39606 . . . . 5 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2 idn2 39604 . . . . . 6 (   𝜑   ,   𝜓   ▶   𝜓   )
3 idn1 39556 . . . . . . 7 (   𝜑   ▶   𝜑   )
4 exbiriVD.1 . . . . . . 7 ((𝜑𝜓) → (𝜒𝜃))
5 pm3.3 440 . . . . . . . 8 (((𝜑𝜓) → (𝜒𝜃)) → (𝜑 → (𝜓 → (𝜒𝜃))))
65com12 32 . . . . . . 7 (𝜑 → (((𝜑𝜓) → (𝜒𝜃)) → (𝜓 → (𝜒𝜃))))
73, 4, 6e10 39685 . . . . . 6 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
8 pm2.27 42 . . . . . 6 (𝜓 → ((𝜓 → (𝜒𝜃)) → (𝜒𝜃)))
92, 7, 8e21 39722 . . . . 5 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
10 biimpr 212 . . . . . 6 ((𝜒𝜃) → (𝜃𝜒))
1110com12 32 . . . . 5 (𝜃 → ((𝜒𝜃) → 𝜒))
121, 9, 11e32 39750 . . . 4 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
1312in3 39600 . . 3 (   𝜑   ,   𝜓   ▶   (𝜃𝜒)   )
1413in2 39596 . 2 (   𝜑   ▶   (𝜓 → (𝜃𝜒))   )
1514in1 39553 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385
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 199  df-an 386  df-3an 1110  df-vd1 39552  df-vd2 39560  df-vd3 39572
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator