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 41056
Description: Virtual deduction proof of exbiri 807. 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 40896 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
6:3,5,?: e21 40932 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
7:4,6,?: e32 40960 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
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 40817 . . . . 5 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2 idn2 40815 . . . . . 6 (   𝜑   ,   𝜓   ▶   𝜓   )
3 idn1 40776 . . . . . . 7 (   𝜑   ▶   𝜑   )
4 exbiriVD.1 . . . . . . 7 ((𝜑𝜓) → (𝜒𝜃))
5 pm3.3 449 . . . . . . . 8 (((𝜑𝜓) → (𝜒𝜃)) → (𝜑 → (𝜓 → (𝜒𝜃))))
65com12 32 . . . . . . 7 (𝜑 → (((𝜑𝜓) → (𝜒𝜃)) → (𝜓 → (𝜒𝜃))))
73, 4, 6e10 40896 . . . . . 6 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
8 pm2.27 42 . . . . . 6 (𝜓 → ((𝜓 → (𝜒𝜃)) → (𝜒𝜃)))
92, 7, 8e21 40932 . . . . 5 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
10 biimpr 221 . . . . . 6 ((𝜒𝜃) → (𝜃𝜒))
1110com12 32 . . . . 5 (𝜃 → ((𝜒𝜃) → 𝜒))
121, 9, 11e32 40960 . . . 4 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
1312in3 40811 . . 3 (   𝜑   ,   𝜓   ▶   (𝜃𝜒)   )
1413in2 40807 . 2 (   𝜑   ▶   (𝜓 → (𝜃𝜒))   )
1514in1 40773 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397  df-3an 1083  df-vd1 40772  df-vd2 40780  df-vd3 40792
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator