Users' Mathboxes 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 32699
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 205 . . 3 ((𝜃𝜏) → (𝜃𝜏))
21imim1i 63 . 2 (((𝜃𝜏) → 𝜑) → ((𝜃𝜏) → 𝜑))
3 biimpr 210 . . 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 196
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
This theorem is referenced by:  bj-bisym  32700
  Copyright terms: Public domain W3C validator