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 39403
Description: Virtual deduction proof of exbiri 651. 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 39236 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
6:3,5,?: e21 39274 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
7:4,6,?: e32 39302 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
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 39157 . . . . 5 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2 idn2 39155 . . . . . 6 (   𝜑   ,   𝜓   ▶   𝜓   )
3 idn1 39107 . . . . . . 7 (   𝜑   ▶   𝜑   )
4 exbiriVD.1 . . . . . . 7 ((𝜑𝜓) → (𝜒𝜃))
5 pm3.3 459 . . . . . . . 8 (((𝜑𝜓) → (𝜒𝜃)) → (𝜑 → (𝜓 → (𝜒𝜃))))
65com12 32 . . . . . . 7 (𝜑 → (((𝜑𝜓) → (𝜒𝜃)) → (𝜓 → (𝜒𝜃))))
73, 4, 6e10 39236 . . . . . 6 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
8 pm2.27 42 . . . . . 6 (𝜓 → ((𝜓 → (𝜒𝜃)) → (𝜒𝜃)))
92, 7, 8e21 39274 . . . . 5 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
10 biimpr 210 . . . . . 6 ((𝜒𝜃) → (𝜃𝜒))
1110com12 32 . . . . 5 (𝜃 → ((𝜒𝜃) → 𝜒))
121, 9, 11e32 39302 . . . 4 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
1312in3 39151 . . 3 (   𝜑   ,   𝜓   ▶   (𝜃𝜒)   )
1413in2 39147 . 2 (   𝜑   ▶   (𝜓 → (𝜃𝜒))   )
1514in1 39104 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 385  df-3an 1056  df-vd1 39103  df-vd2 39111  df-vd3 39123
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator