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

Theorem imbi13 37747
 Description: Join three logical equivalences to form equivalence of implications. imbi13 37747 is imbi13VD 38132 without virtual deductions and was automatically derived from imbi13VD 38132 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
imbi13 ((𝜑𝜓) → ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂))))))

Proof of Theorem imbi13
StepHypRef Expression
1 imbi12 335 . 2 ((𝜒𝜃) → ((𝜏𝜂) → ((𝜒𝜏) ↔ (𝜃𝜂))))
2 imbi12 335 . 2 ((𝜑𝜓) → (((𝜒𝜏) ↔ (𝜃𝜂)) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂)))))
31, 2syl9r 76 1 ((𝜑𝜓) → ((𝜒𝜃) → ((𝜏𝜂) → ((𝜑 → (𝜒𝜏)) ↔ (𝜓 → (𝜃𝜂))))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 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 196 This theorem is referenced by:  trsbc  37771  trsbcVD  38135
 Copyright terms: Public domain W3C validator