Mathbox for Wolf Lammen 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > wlembantd  Structured version Unicode version 
Description: Deduction version of wlembant 29901. Generalization of a2i 13, imim12i 57, imim1i 58 and imim2i 14, which can be proved by specializing its hypotheses, and some trivial rearrangements. This theorem clarifies in a more general way, under what conditions a wff may be introduced as a nested antecedent to an antecedent. Note: this theorem is not intuitionistically valid (see embantd 54). (Contributed by Wolf Lammen, 4Oct2013.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

wlembantd.1  
wlembantd.2 
Ref  Expression 

wlembantd 
Step  Hyp  Ref  Expression 

1  wlembantd.1  . . 3  
2  1  pm2.24d 143  . 2 
3  wlembantd.2  . 2  
4  2, 3  jad 162  1 
Colors of variables: wff setvar class 
Syntax hints: wi 4 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem is referenced by: (None) 
Copyright terms: Public domain  W3C validator 