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 38611
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 38440 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
6:3,5,?: e21 38478 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
7:4,6,?: e32 38506 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
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 38361 . . . . 5 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜃   )
2 idn2 38359 . . . . . 6 (   𝜑   ,   𝜓   ▶   𝜓   )
3 idn1 38311 . . . . . . 7 (   𝜑   ▶   𝜑   )
4 exbiriVD.1 . . . . . . 7 ((𝜑𝜓) → (𝜒𝜃))
5 pm3.3 460 . . . . . . . 8 (((𝜑𝜓) → (𝜒𝜃)) → (𝜑 → (𝜓 → (𝜒𝜃))))
65com12 32 . . . . . . 7 (𝜑 → (((𝜑𝜓) → (𝜒𝜃)) → (𝜓 → (𝜒𝜃))))
73, 4, 6e10 38440 . . . . . 6 (   𝜑   ▶   (𝜓 → (𝜒𝜃))   )
8 pm2.27 42 . . . . . 6 (𝜓 → ((𝜓 → (𝜒𝜃)) → (𝜒𝜃)))
92, 7, 8e21 38478 . . . . 5 (   𝜑   ,   𝜓   ▶   (𝜒𝜃)   )
10 biimpr 210 . . . . . 6 ((𝜒𝜃) → (𝜃𝜒))
1110com12 32 . . . . 5 (𝜃 → ((𝜒𝜃) → 𝜒))
121, 9, 11e32 38506 . . . 4 (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
1312in3 38355 . . 3 (   𝜑   ,   𝜓   ▶   (𝜃𝜒)   )
1413in2 38351 . 2 (   𝜑   ▶   (𝜓 → (𝜃𝜒))   )
1514in1 38308 1 (𝜑 → (𝜓 → (𝜃𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386  df-3an 1038  df-vd1 38307  df-vd2 38315  df-vd3 38327
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator