NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ee10 GIF version

Theorem ee10 1376
Description: e10 in set.mm without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) TODO: this is frequently used; come up with better label.
Hypotheses
Ref Expression
ee10.1 (φψ)
ee10.2 χ
ee10.3 (ψ → (χθ))
Assertion
Ref Expression
ee10 (φθ)

Proof of Theorem ee10
StepHypRef Expression
1 ee10.1 . 2 (φψ)
2 ee10.2 . . 3 χ
3 ee10.3 . . 3 (ψ → (χθ))
42, 3mpi 16 . 2 (ψθ)
51, 4syl 15 1 (φθ)
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  ceqsex  2893  moeq3  3013
  Copyright terms: Public domain W3C validator