New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > imim12d | GIF version |
Description: Deduction combining antecedents and consequents. (Contributed by NM, 7-Aug-1994.) (Proof shortened by O'Cat, 30-Oct-2011.) |
Ref | Expression |
---|---|
imim12d.1 | ⊢ (φ → (ψ → χ)) |
imim12d.2 | ⊢ (φ → (θ → τ)) |
Ref | Expression |
---|---|
imim12d | ⊢ (φ → ((χ → θ) → (ψ → τ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim12d.1 | . 2 ⊢ (φ → (ψ → χ)) | |
2 | imim12d.2 | . . 3 ⊢ (φ → (θ → τ)) | |
3 | 2 | imim2d 48 | . 2 ⊢ (φ → ((χ → θ) → (χ → τ))) |
4 | 1, 3 | syl5d 62 | 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: imim1d 69 equveli 1988 mo 2226 rspcimdv 2956 |
Copyright terms: Public domain | W3C validator |