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

Theorem imbi13VD 44452
Description: Join three logical equivalences to form equivalence of implications. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi13 44098 is imbi13VD 44452 without virtual deductions and was automatically derived from imbi13VD 44452.
1:: (   (𝜑𝜓)   ▶   (𝜑𝜓)   )
2:: (   (𝜑𝜓)   ,   (𝜒𝜃)    ▶   (𝜒𝜃)   )
3:: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜏 𝜂)   ▶   (𝜏𝜂)   )
4:2,3: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜏 𝜂)   ▶   ((𝜒𝜏) ↔ (𝜃𝜂))   )
5:1,4: (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜏 𝜂)   ▶   ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂)))   )
6:5: (   (𝜑𝜓)   ,   (𝜒𝜃)    ▶   ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃 𝜂))))   )
7:6: (   (𝜑𝜓)   ▶   ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃 𝜂)))))   )
qed:7: ((𝜑𝜓) → ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃 𝜂))))))
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
imbi13VD ((𝜑𝜓) → ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂))))))

Proof of Theorem imbi13VD
StepHypRef Expression
1 idn1 44152 . . . . 5 (   (𝜑𝜓)   ▶   (𝜑𝜓)   )
2 idn2 44191 . . . . . 6 (   (𝜑𝜓)   ,   (𝜒𝜃)   ▶   (𝜒𝜃)   )
3 idn3 44193 . . . . . 6 (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜏𝜂)   ▶   (𝜏𝜂)   )
4 imbi12 345 . . . . . 6 ((𝜒𝜃) → ((𝜏𝜂) → ((𝜒𝜏) ↔ (𝜃𝜂))))
52, 3, 4e23 44333 . . . . 5 (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜏𝜂)   ▶   ((𝜒𝜏) ↔ (𝜃𝜂))   )
6 imbi12 345 . . . . 5 ((𝜑𝜓) → (((𝜒𝜏) ↔ (𝜃𝜂)) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂)))))
71, 5, 6e13 44326 . . . 4 (   (𝜑𝜓)   ,   (𝜒𝜃)   ,   (𝜏𝜂)   ▶   ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂)))   )
87in3 44187 . . 3 (   (𝜑𝜓)   ,   (𝜒𝜃)   ▶   ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂))))   )
98in2 44183 . 2 (   (𝜑𝜓)   ▶   ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂)))))   )
109in1 44149 1 ((𝜑𝜓) → ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206  df-an 395  df-3an 1086  df-vd1 44148  df-vd2 44156  df-vd3 44168
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator