Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj835 Structured version   Visualization version   GIF version

Theorem bnj835 31678
Description: -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj835.1 (𝜂 ↔ (𝜑𝜓𝜒))
bnj835.2 (𝜑𝜏)
Assertion
Ref Expression
bnj835 (𝜂𝜏)

Proof of Theorem bnj835
StepHypRef Expression
1 bnj835.1 . 2 (𝜂 ↔ (𝜑𝜓𝜒))
2 bnj835.2 . . 3 (𝜑𝜏)
323ad2ant1 1113 . 2 ((𝜑𝜓𝜒) → 𝜏)
41, 3sylbi 209 1 (𝜂𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  w3a 1068
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 199  df-an 388  df-3an 1070
This theorem is referenced by:  bnj1219  31720  bnj1379  31750  bnj1175  31921  bnj1286  31936  bnj1280  31937  bnj1296  31938  bnj1398  31951  bnj1415  31955  bnj1417  31958  bnj1421  31959  bnj1442  31966  bnj1450  31967  bnj1452  31969  bnj1489  31973  bnj1312  31975  bnj1501  31984  bnj1523  31988
  Copyright terms: Public domain W3C validator