Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-bi3ant Structured version   Visualization version   GIF version

Theorem bj-bi3ant 34317
 Description: This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013.) (Revised by BJ, 14-Jun-2019.)
Hypothesis
Ref Expression
bj-bi3ant.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
bj-bi3ant (((𝜃𝜏) → 𝜑) → (((𝜏𝜃) → 𝜓) → ((𝜃𝜏) → 𝜒)))

Proof of Theorem bj-bi3ant
StepHypRef Expression
1 biimp 218 . . 3 ((𝜃𝜏) → (𝜃𝜏))
21imim1i 63 . 2 (((𝜃𝜏) → 𝜑) → ((𝜃𝜏) → 𝜑))
3 biimpr 223 . . 3 ((𝜃𝜏) → (𝜏𝜃))
43imim1i 63 . 2 (((𝜏𝜃) → 𝜓) → ((𝜃𝜏) → 𝜓))
5 bj-bi3ant.1 . . 3 (𝜑 → (𝜓𝜒))
65imim3i 64 . 2 (((𝜃𝜏) → 𝜑) → (((𝜃𝜏) → 𝜓) → ((𝜃𝜏) → 𝜒)))
72, 4, 6syl2im 40 1 (((𝜃𝜏) → 𝜑) → (((𝜏𝜃) → 𝜓) → ((𝜃𝜏) → 𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  bj-bisym  34318
 Copyright terms: Public domain W3C validator