![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imim12d | Structured version Visualization version GIF version |
Description: Deduction combining antecedents and consequents. Deduction associated with imim12 105 and imim12i 62. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mel L. 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 57 | . 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜒 → 𝜏))) |
4 | 1, 3 | syl5d 73 | 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 82 orim12dALT 910 nfimd 1897 axc15 2421 ax9ALT 2727 rspcimdv 3602 peano5 7886 peano5OLD 7887 isf34lem6 10377 inar1 10772 supsrlem 11108 r19.29uz 15301 o1of2 15561 o1rlimmul 15567 caucvg 15629 isprm5 16648 mrissmrid 17589 kgen2ss 23279 txlm 23372 isr0 23461 metcnpi3 24275 addcnlem 24600 nmhmcn 24860 aalioulem5 26073 xrlimcnp 26697 dmdmd 31808 mdsl0 31818 mdsl1i 31829 lmxrge0 33218 bnj517 34182 ax8dfeq 35062 poimirlem29 36820 heicant 36826 ispridlc 37241 dffltz 41678 intabssd 42572 ss2iundf 42712 ismnushort 43362 |
Copyright terms: Public domain | W3C validator |