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 29889
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 1074 . 2 ((𝜑𝜓𝜒) → 𝜏)
41, 3sylbi 205 1 (𝜂𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  bnj1219  29931  bnj1379  29961  bnj1175  30132  bnj1286  30147  bnj1280  30148  bnj1296  30149  bnj1398  30162  bnj1415  30166  bnj1417  30169  bnj1421  30170  bnj1442  30177  bnj1450  30178  bnj1452  30180  bnj1489  30184  bnj1312  30186  bnj1501  30195  bnj1523  30199
  Copyright terms: Public domain W3C validator