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 rspcimdv 3310 peano5 7089 isf34lem6 9202 inar1 9597 supsrlem 9932 r19.29uz 14090 o1of2 14343 o1rlimmul 14349 caucvg 14409 isprm5 15419 mrissmrid 16301 kgen2ss 21358 txlm 21451 isr0 21540 metcnpi3 22351 addcnlem 22667 nmhmcn 22920 aalioulem5 24091 xrlimcnp 24695 dmdmd 29159 mdsl0 29169 mdsl1i 29180 lmxrge0 29998 bnj517 30955 ax8dfeq 31704 bj-mo3OLD 32832 bj-ax9-2 32891 poimirlem29 33438 heicant 33444 ispridlc 33869 intabssd 37916 ss2iundf 37951 |
Copyright terms: Public domain | W3C validator |