|   | Mathbox for Alan Sare | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > dfvd2i | Structured version Visualization version GIF version | ||
| Description: Inference form of dfvd2 44599. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| dfvd2i.1 | ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | 
| Ref | Expression | 
|---|---|
| dfvd2i | ⊢ (𝜑 → (𝜓 → 𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | dfvd2i.1 | . 2 ⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) | |
| 2 | dfvd2 44599 | . 2 ⊢ (( 𝜑 , 𝜓 ▶ 𝜒 ) ↔ (𝜑 → (𝜓 → 𝜒))) | |
| 3 | 1, 2 | mpbi 230 | 1 ⊢ (𝜑 → (𝜓 → 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ( wvd2 44597 | 
| 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 207 df-an 396 df-vd2 44598 | 
| This theorem is referenced by: vd23 44622 in2 44625 in2an 44628 gen21 44639 gen21nv 44640 gen22 44642 exinst 44644 exinst01 44645 exinst11 44646 e2 44651 e222 44656 e233 44785 e323 44786 | 
| Copyright terms: Public domain | W3C validator |