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 32258
 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 1130 . 2 ((𝜑𝜓𝜒) → 𝜏)
41, 3sylbi 220 1 (𝜂𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084 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  df-an 400  df-3an 1086 This theorem is referenced by:  bnj1219  32300  bnj1379  32330  bnj1175  32504  bnj1286  32519  bnj1280  32520  bnj1296  32521  bnj1398  32534  bnj1415  32538  bnj1417  32541  bnj1421  32542  bnj1442  32549  bnj1450  32550  bnj1452  32552  bnj1489  32556  bnj1312  32558  bnj1501  32567  bnj1523  32571
 Copyright terms: Public domain W3C validator