Description: Firstorder logic and set theory. (Contributed by Jonathan BenNaim, 3Jun2011) (New usage is discouraged.)
Ref  Expression  

Hypotheses  bnj1276.1   ( ph > A. x ph ) 

bnj1276.2   ( ps > A. x ps ) 

bnj1276.3   ( ch > A. x ch ) 

bnj1276.4   ( th <> ( ph /\ ps /\ ch ) ) 

Assertion  bnj1276   ( th > A. x th ) 
Step  Hyp  Ref  Expression 

1  bnj1276.1   ( ph > A. x ph ) 

2  bnj1276.2   ( ps > A. x ps ) 

3  bnj1276.3   ( ch > A. x ch ) 

4  bnj1276.4   ( th <> ( ph /\ ps /\ ch ) ) 

5  1 2 3  hb3an   ( ( ph /\ ps /\ ch ) > A. x ( ph /\ ps /\ ch ) ) 
6  4 5  hbxfrbi   ( th > A. x th ) 